Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10,454 changes: 5,244 additions & 5,210 deletions generated/mhs.c

Large diffs are not rendered by default.

14 changes: 14 additions & 0 deletions lib/Data/TypeLits.hs
Original file line number Diff line number Diff line change
Expand Up @@ -3,15 +3,29 @@ module Data.TypeLits(
Nat,
KnownNat(..),
KnownSymbol(..),
SymbolEq,
AppendSymbol,
ConsSymbol
) where
import qualified Prelude()
import Primitives
import Data.Char_Type
import Data.Integer
import {-# SOURCE #-} Data.Typeable

-- Special classes solved by the typechecker.
-- An instance of one of these classes would be useless.

class KnownNat (n :: Nat) where
natVal :: forall (proxy :: Nat -> Type) . proxy n -> Integer

class KnownSymbol (s :: Symbol) where
symbolVal :: forall (proxy :: Symbol -> Type) . proxy s -> String

-- Tests two litteral Symbols equality and returns "True" or "False".
class SymbolEq (s :: Symbol) (t :: Symbol) (b :: Symbol) | s t -> b

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this what GHC does? I try to be compatible.

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Title: GHC-compatible AppendSymbol (and possibly CmpSymbol) for Data.TypeLits

Motivation

MicroHs already supports Symbol, KnownSymbol, and symbolVal, resolved
specially in TypeCheck.hs (the solvers table, alongside KnownNat and
Coercible). This makes a lot of type-level Symbol programming possible, but
one common building block from GHC.TypeLits is still missing:
AppendSymbol.

In GHC, AppendSymbol is declared as a closed type family with no visible
equations — its reduction is entirely wired into the constraint
solver/normalizer, not written in user-level Haskell:

type family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol

Crucially, it is used inline, in type position, and reduces during
unification wherever it appears, e.g.:

f :: Proxy (AppendSymbol "foo" "bar") -> ...

What I tried as a workaround

Without DataKinds or general type families, I prototyped AppendSymbol (and
a couple of related primitives, ConsSymbol and SymbolEq) as an ordinary
multi-parameter class with functional dependencies, resolved specially by the
typechecker exactly like KnownSymbol/Coercible are — i.e. intercepted in
the solvers table by class name, before falling through to solveInst:

class AppendSymbol (s :: Symbol) (t :: Symbol) (st :: Symbol)
  | s t -> st, st t -> s, st s -> t
solveAppendSymbol :: SolveOne
solveAppendSymbol loc iCls [s, t, st] = ...
  -- pattern-matches on ELit (LStr ...) literals, computes the concatenation
  -- or the missing side (given the other two), unifies via Improve, or
  -- errors out on a literal mismatch
solveAppendSymbol loc iCls ts = solveInst loc iCls ts

This works well as a relation: it can check, complete, or reject a triple
of Symbols at compile time, with proper deferral when one side is still a
unification variable. (Happy to share the full patch — it also required a
ConsSymbol h t s primitive for structural decomposition of a literal
Symbol, and a SymbolEq s t b primitive returning "True"/"False" as
disjoint literals, needed to route around what looks like a specificity gap
in instance selection between a concrete Symbol literal and a type
variable — getBestMatches/findMatches in TypeCheck.hs did not seem to
prefer the more specific literal instance over a fully polymorphic one, even
with OverlappingInstances enabled.)

Where this workaround falls short

A class-based relation can never be GHC-compatible in the way
AppendSymbol is normally used, because AppendSymbol "foo" "bar" in GHC is
a type-level expression that reduces to "foobar" wherever it occurs — it
is not merely related to it through an external constraint. Concretely, code
that expects to write Proxy (AppendSymbol "foo" "bar") inline, or to nest
AppendSymbol inside a bigger type, cannot be made to work through a
class/fundep encoding; only three separate, explicitly-threaded type
variables with a constraint between them are possible that way. Since
"a type-level application that reduces during unification" is definitionally
what a type family is (whether user-defined or, as here, wired into the
compiler with no equations), matching GHC's actual AppendSymbol seems to
require some form of type family support, even a very restricted one.

Proposed scope

Given MicroHs's stated goal of GHC compatibility, and that a similarly
special-cased mechanism already exists for KnownSymbol/KnownNat/
Coercible, would you be open to a narrowly-scoped patch that:

  1. Parses a closed, equation-free type family signature —
    type family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol — without
    supporting the general type family machinery (open families, user
    equations, associated families, etc.).
  2. Registers AppendSymbol with kind Symbol -> Symbol -> Symbol in the
    kind checker.
  3. Recognizes AppendSymbol lit1 lit2 (both Symbol literals) during type
    normalization/unification (unifyR, or an expandSyn-like pass run
    beforehand) and reduces it directly to the concatenated literal, deferring
    via the existing unification-variable machinery when one side isn't a
    literal yet.

This would be intentionally much narrower than general TypeFamilies
support — closer in spirit to how AppendSymbol itself is "wired in" rather
than user-defined in GHC — and could plausibly extend later to CmpSymbol
if useful, following the same pattern.

If this is out of scope for MicroHs's design goals, the class/fundep
workaround above is a perfectly usable substitute for most purposes (proving
and computing Symbol relations at compile time) — it just can't be a drop-in
replacement for code written against GHC.TypeLits.AppendSymbol syntax.

Happy to share the full prototype (AppendSymbol/ConsSymbol/SymbolEq +
TypeCheck.hs solvers) if useful as a starting point, and to help test a
patch along these lines if you'd like to attempt it.


class AppendSymbol (s :: Symbol) (t :: Symbol) (st :: Symbol) | s t -> st, st s -> t, st t -> s

class ConsSymbol (h :: Symbol) (t :: Symbol) (s :: Symbol)
| h t -> s, s -> h t
83 changes: 83 additions & 0 deletions mhs.conf
Original file line number Diff line number Diff line change
@@ -0,0 +1,83 @@
-- mhs keys
-- packageDbPath package lookup path
-- The path is expanded from the environment.
-- $MHSPKG is always the package directory relative
-- to the mhs binary, and $VERSION is the compiler version.
[mhs]
packageDbPath = "$MHSPKG:$HOME/.mcabal-user/mhs-$VERSION"

-- Target keys
-- cc C compiler to use, default "cc"
-- ccflags flags to pass at the beginning of the compiler command, default ""
-- cclibs flags to pass at the end of the compilation command, default ""
-- conf the config directory to use, default "unix"
-- cout flag to set the output file to cc, default "-o"

-- If no target is set, we use 'unix' on non-Windows and 'windows' on Windows.

-- Typical Unix-like flags
-- Assumes gcc or clang
[unix]
cc = "cc"
ccflags = "-w -Wall -O3 "
cclibs = " -lm"
conf = "unix"

-- As above, but with -flto
-- This flag improves performance, but generates a warning with gcc.
[unix_lto]
cc = "cc"
ccflags = "-w -Wall -O3 -flto "
cclibs = " -lm"
conf = "unix"

-- As above, but with the non-portable flag -march=native
[unix_x86]
cc = "cc"
ccflags = "-w -Wall -O3 -flto -march=native "
cclibs = " -lm"
conf = "unix"

-- Compile with debugging instead of optimization
[debug]
cc = "cc"
ccflags = "-w -Wall -g"
cclibs = "-lm"
conf = "unix"

-- Generate JavaScript&Wasm
[emscripten]
cc = "emcc"
ccflags = "-O3 -sEXPORTED_RUNTIME_METHODS=stringToNewUTF8 -sALLOW_MEMORY_GROWTH -sTOTAL_STACK=5MB -sNODERAWFS -sSINGLE_FILE -DUSE_SYSTEM_RAW -sEXIT_RUNTIME -Wno-address-of-packed-member"
cclibs = "-lm"
conf = "unix"

-- Generate JavaScript&Wasm, with xterm.js support
[emscripten_web]
cc = "emcc"
ccflags = "-O3 -sASYNCIFY -sEXPORTED_FUNCTIONS=['_main','_set_input_char'] -sEXPORTED_RUNTIME_METHODS=['FS','ccall'] -sFORCE_FILESYSTEM=1 -sALLOW_MEMORY_GROWTH -sTOTAL_STACK=5MB -DUSE_WEB_INPUT -Wno-address-of-packed-member"
cclibs = "-lm"
conf = "unix"

-- Use the Tiny C Compiler
[tcc]
cc = "tcc"
ccflags = "-D__TCC__=1"
cclibs = "-lm"
conf = "unix"

-- Windows flags, with stdout supressed
[windows]
cc = "cl > NUL /nologo"
ccflags = "-O2"
cclibs = ""
conf = "windows"
cout = "-Fe"

-- Take all flags from environment variables
[environment]
-- Get all values from the environment
cc = "$CC"
ccflags = "$MHSCCFLAGS"
cclibs = "$MHSCCLIBS"
conf = "$MHSCONF"
9 changes: 9 additions & 0 deletions src/MicroHs/Names.hs
Original file line number Diff line number Diff line change
Expand Up @@ -100,6 +100,15 @@ nameKnownNat = "Data.TypeLits.KnownNat"
nameKnownSymbol :: String
nameKnownSymbol = "Data.TypeLits.KnownSymbol"

nameSymbolEq :: String
nameSymbolEq = "Data.TypeLits.SymbolEq"

nameAppendSymbol :: String
nameAppendSymbol = "Data.TypeLits.AppendSymbol"

nameConsSymbol :: String
nameConsSymbol = "Data.TypeLits.ConsSymbol"

nameDataTypeableTypeable :: String
nameDataTypeableTypeable = "Data.Typeable.Typeable"
identDataTypeableTypeable :: Ident
Expand Down
69 changes: 69 additions & 0 deletions src/MicroHs/TypeCheck.hs
Original file line number Diff line number Diff line change
Expand Up @@ -3592,6 +3592,9 @@ solvers =
, ((== mkIdent nameTypeEq), solveTypeEq) -- handle equality constraints, i.e. (t1 ~ t2)
, ((== mkIdent nameKnownNat), solveKnownNat) -- KnownNat 123 constraints
, ((== mkIdent nameKnownSymbol), solveKnownSymbol) -- KnownSymbol "abc" constraints
, ((== mkIdent nameSymbolEq), solveSymbolEq) -- SymbolEq "hello" "h3ll0" "False"
, ((== mkIdent nameAppendSymbol),solveAppendSymbol) -- AppendSymbol "ab" "cd" "abcd" constraints
, ((== mkIdent nameConsSymbol), solveConsSymbol) -- ConsSymbol "h" "tail" "htail" ("h" always 1 character) contraints
, ((== mkIdent nameCoercible), solveCoercible) -- Coercible a b constraints
, (const True, solveInst) -- handle constraints with instances
]
Expand Down Expand Up @@ -3777,6 +3780,72 @@ solveKnownSymbol :: SolveOne
solveKnownSymbol loc iCls [e@(ELit _ (LStr _))] = mkConstDict loc iCls e
solveKnownSymbol loc iCls ts = solveInst loc iCls ts -- look for a dict argument

solveSymbolEq :: SolveOne
solveSymbolEq loc iCls [s, t, b] =
case (s, t) of
(ELit _ (LStr sStr), ELit _ (LStr tStr)) ->
let result = if sStr == tStr then "True" else "False"
in case b of
ELit _ (LStr bStr)
| bStr == result -> return $ Just (ETuple [], [], [])
| otherwise -> return Nothing
_ | isEUVar b -> return $ Just (ETuple [], [], [(loc, b, ELit loc (LStr result))])
| otherwise -> return Nothing
_ -> solveInst loc iCls [s, t, b] -- s ou t pas encore concrets : on defere

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

English, please

solveSymbolEq loc iCls ts = solveInst loc iCls ts

solveAppendSymbol :: SolveOne
solveAppendSymbol loc iCls [s, t, st] =
case (getLit s, getLit t, getLit st) of
(Just sStr, Just tStr, _) ->
unifyOrCheck loc st (sStr ++ tStr)
(Just sStr, Nothing, Just stStr)
| sStr `isPrefixOf` stStr -> unifyOrCheck loc t (drop (length sStr) stStr)
| otherwise -> tcError loc $ "AppendSymbol: " ++ show stStr
++ " does not start with " ++ show sStr
(Nothing, Just tStr, Just stStr)
| tStr `isSuffixOf` stStr -> unifyOrCheck loc s (take (length stStr - length tStr) stStr)
| otherwise -> tcError loc $ "AppendSymbol: " ++ show stStr
++ " does not end with " ++ show tStr
_ -> solveInst loc iCls [s, t, st] -- not enough info : we defere

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Spelling

where
getLit (ELit _ (LStr x)) = Just x
getLit _ = Nothing
unifyOrCheck l ty target = case ty of
ELit _ (LStr actual) | actual == target -> return $ Just (ETuple [], [], [])
| otherwise -> tcError l $ "AppendSymbol mismatch"
_ | isEUVar ty -> return $ Just (ETuple [], [], [(l, ty, ELit l (LStr target))])
| otherwise -> return Nothing
solveAppendSymbol loc iCls ts = solveInst loc iCls ts

solveConsSymbol :: SolveOne
-- Case 1 : s already known -> we split a head (1 character) and a tail
solveConsSymbol loc iCls [h, t, s@(ELit _ (LStr sStr))]
| null sStr = return Nothing -- empty Symbol has neither head nor tail
| otherwise = do
let hStr = take 1 sStr
tStr = drop 1 sStr
check ty target = case ty of
ELit _ (LStr actual)
| actual == target -> Right []
| otherwise -> Left actual
_ | isEUVar ty -> Right [(loc, ty, ELit loc (LStr target))]
| otherwise -> Right []
case (check h hStr, check t tStr) of
(Left actual, _) ->
tcError loc $ "ConsSymbol: expected head " ++ show hStr ++ ", received " ++ show actual
(_, Left actual) ->
tcError loc $ "ConsSymbol: expected tail " ++ show tStr ++ ", received " ++ show actual
(Right is1, Right is2) -> return $ Just (ETuple [], [], is1 ++ is2)
-- Case 2 : h and t already known (and s not litteral, otherwise case 1 should match)
solveConsSymbol loc iCls [h@(ELit _ (LStr hStr)), t@(ELit _ (LStr tStr)), s]
| length hStr /= 1 =
tcError loc $ "ConsSymbol: head should be 1 character, received " ++ show hStr
| isEUVar s = return $ Just (ETuple [], [], [(loc, s, ELit loc (LStr (hStr ++ tStr)))])
| otherwise = return Nothing
-- not enough info : we defer
solveConsSymbol loc iCls ts = solveInst loc iCls ts

mkConstDict :: SLoc -> Ident -> Expr -> T (Maybe (Expr, [Goal], [Improve]))
mkConstDict loc iCls e = do
let res = EApp (EVar $ mkClassConstructor iCls) fcn
Expand Down
29 changes: 29 additions & 0 deletions tests/AppendSymbol.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
module AppendSymbol where
import Data.Proxy
import Data.TypeLits

testSuccess :: AppendSymbol "ab" "cd" "abcd" => Bool
testSuccess = True

testAppend :: AppendSymbol s1 s2 s3 => Proxy s1 -> Proxy s2 -> Proxy s3
testAppend _ _ = Proxy

testPrefix :: AppendSymbol s1 s2 s3 => Proxy s3 -> Proxy s2 -> Proxy s1
testPrefix _ _ = Proxy

testSuffix :: AppendSymbol s1 s2 s3 => Proxy s3 -> Proxy s1 -> Proxy s2
testSuffix _ _ = Proxy

testChain ::
( AppendSymbol s1 s2 s3
, AppendSymbol s3 s4 s7)
=> Proxy s1 -> Proxy s2 -> Proxy s4 -> Proxy s7
testChain _ _ _ = Proxy

main = do
putStrLn $ show testSuccess
putStrLn $ symbolVal $ testAppend (Proxy :: Proxy "ab") (Proxy :: Proxy "cd")
putStrLn $ symbolVal $ testPrefix (Proxy :: Proxy "abcd") (Proxy :: Proxy "cd")
putStrLn $ symbolVal $ testSuffix (Proxy :: Proxy "abcd") (Proxy :: Proxy "ab")
putStrLn $ symbolVal $
testChain (Proxy :: Proxy "ab") (Proxy :: Proxy "cd") (Proxy :: Proxy "ef")
5 changes: 5 additions & 0 deletions tests/AppendSymbol.ref
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
True
abcd
ab
cd
abcdef
114 changes: 114 additions & 0 deletions tests/ConsSymbolEq.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,114 @@
module ConsSymbolEq where

import Data.Proxy
import Data.TypeLits (Symbol, KnownSymbol, symbolVal, AppendSymbol, ConsSymbol, SymbolEq)

--------------------------------------------------------------------------------
-- Specifier : Lit wraps a Symbol.
--------------------------------------------------------------------------------

data D -- digit
data S -- string
data Lit (lit :: Symbol)

class Specifier s
instance Specifier D
instance Specifier S
instance (KnownSymbol lit) => Specifier (Lit lit)

--------------------------------------------------------------------------------
-- FList : lists the formats.
--------------------------------------------------------------------------------

data FNil
data FCons s fl

class FList fl
instance FList FNil
instance (Specifier s, FList fl) => FList (FCons s fl)

--------------------------------------------------------------------------------
-- FormatF : splits the %d / %s formats
--------------------------------------------------------------------------------

class (FList format) => FormatF format fun | format -> fun where
formatF :: Proxy format -> String -> fun

instance FormatF FNil String where
formatF _ = id

instance (FormatF rest fun)
=> FormatF (FCons D rest) (Int -> fun) where
formatF _ str = \i -> formatF (Proxy :: Proxy rest) (str ++ show i)

instance (FormatF rest fun)
=> FormatF (FCons S rest) (String -> fun) where
formatF _ str = \s -> formatF (Proxy :: Proxy rest) (str ++ s)

instance (KnownSymbol lit, FormatF rest fun)
=> FormatF (FCons (Lit lit) rest) fun where
formatF _ str
= formatF (Proxy :: Proxy rest) (str ++ symbolVal (Proxy :: Proxy lit))

--------------------------------------------------------------------------------
-- MatchFmt
--------------------------------------------------------------------------------

class (Specifier out) => MatchFmt (head :: Symbol) out | head -> out
instance MatchFmt "d" D
instance MatchFmt "s" S

--------------------------------------------------------------------------------
-- Parse : uses SymbolEq -> "True"/"False" to avoid instance overlappings.
--------------------------------------------------------------------------------

class (FList format) => Parse (string :: Symbol) format | string -> format
instance (SymbolEq string "" isEmpty, ParseC isEmpty string format)
=> Parse string format

class (FList out) => ParseC (isEmpty :: Symbol) (string :: Symbol) out | isEmpty string -> out

instance ParseC "True" string (FCons (Lit "") FNil)

instance (ConsSymbol h t string, Match h t out)
=> ParseC "False" string out

--------------------------------------------------------------------------------
-- Match : uses SymbolEq also.
--------------------------------------------------------------------------------

class (FList out) => Match (h :: Symbol) (t :: Symbol) out | h t -> out
instance (SymbolEq h "%" isPct, MatchC isPct h t out)
=> Match h t out

class (FList out) => MatchC (isPct :: Symbol) (h :: Symbol) (t :: Symbol) out
| isPct h t -> out

-- '%' : on decompose t pour recuperer le caractere de specification (h2)
-- et le reste (t2)
instance (ConsSymbol h2 t2 t, MatchFmt h2 spec, Parse t2 rest)
=> MatchC "True" h t (FCons (Lit "") (FCons spec rest))

-- caractere ordinaire : accumule via AppendSymbol (h prefixe acc)
instance (FList r, KnownSymbol acc', AppendSymbol h acc acc', Parse t (FCons (Lit acc) r))
=> MatchC "False" h t (FCons (Lit acc') r)

--------------------------------------------------------------------------------
-- Format
--------------------------------------------------------------------------------

class Format (string :: Symbol) fun | string -> fun where
format :: Proxy string -> fun

instance (Parse string format, FormatF format fun)
=> Format string fun where
format _ = formatF (Proxy :: Proxy format) ""

--------------------------------------------------------------------------------
-- Exemple
--------------------------------------------------------------------------------

main :: IO ()
main = do
let formatted = format (Proxy :: Proxy "Hi %s! You are %d") "Bill" 12
putStrLn formatted -- "Hi Bill! You are 12"
1 change: 1 addition & 0 deletions tests/ConsSymbolEq.ref
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Hi Bill! You are 12
Loading