data Adt a b c = Foo a | Bar | Baz b c
Types and Typeclasses
Types enable humans and computers to reason about our programs. The halting problem is not a problem, because types can prove code must terminate. They can do even more and prove a program terminates with the right answer: for example, we can prove a given function correctly sorts a list.
Types can automate programming, namely, a human supplies the type of a desired function and the computer programs itself.
Types can be lightweight. Indeed, they can be invisible. A compiler can use type inference to type-check a program completely free of any type annotations. However, it’s good to throw a few type annotations in the source, as they are a form of documentation that is especially reliable because the compiler ensures they stay in sync with the code.
Therefore, we ought to add types to our language. We mimic Haskell, with at least one deliberate difference: let is not generalized. We only generalize top-level definitions.
Typically
We shamelessly lift code from Mark P. Jones, Typing Haskell in Haskell. Our version is simpler because we lack support for mutual recursion and pattern matching.
Since we’re using the Scott encoding, from a data type declaration:
we generate types for the data constructors:
("Foo", a -> Adt a b c)
("Bar", Adt a b c)
("Baz", b -> c -> Adt a b c)
Along with:
("|Foo|Bar|Baz", Adt a b c -> (a -> x) -> x -> (b -> c -> x) -> x)
which represents the type of case in:
case x of Foo a -> f a Bar -> g Baz b c -> h b c
The case keyword is replaced with the identity combinator
during compilation:
I x (\a -> f a) (\ -> g) (\b c -> h b c)
Our type checker is missing several features, such as kind checking and rejecting duplicate definitions.
------------------------------------------------------------------------
-- Type inference.
--
-- `String` is hardcoded to mean `[Int]`.
------------------------------------------------------------------------
infixr 9 .;
infixr 5 ++;
infixl 4 <*> , <$> , <* , *>;
infixl 3 <|>;
infixr 0 $;
undefined = undefined;
($) f x = f x;
id x = x;
flip f x y = f y x;
(&) x f = f x;
data Bool = True | False;
data Maybe a = Nothing | Just a;
fpair p = \f -> case p of { (,) x y -> f x y };
uncurry f p = case p of { (,) x y -> f x y };
fst p = case p of { (,) x y -> x };
snd p = case p of { (,) x y -> y };
first f = uncurry \x y -> (f x, y);
second f = uncurry \x y -> (x, f y);
ife a b c = case a of { True -> b ; False -> c };
not a = case a of { True -> False; False -> True };
(.) f g x = f (g x);
(||) f g = ife f True g;
(&&) f g = ife f g False;
flst xs n c = case xs of { [] -> n; (:) h t -> c h t };
lstEq xs ys = case xs of
{ [] -> flst ys True (\h t -> False)
; (:) x xt -> flst ys False (\y yt -> ife (x == y) (lstEq xt yt) False)
};
foldr c n l = flst l n (\h t -> c h(foldr c n t));
foldl = \f a bs -> foldr (\b g x -> g (f x b)) (\x -> x) bs a;
foldl1 f bs = flst bs undefined (\h t -> foldl f h t);
elem k xs = foldr (\x t -> ife (x == k) True t) False xs;
find f xs = foldr (\x t -> ife (f x) (Just x) t) Nothing xs;
(++) = flip (foldr (:));
concat = foldr (++) [];
wrap c = c:[];
map = flip (foldr . ((:) .)) [];
concatMap = (concat .) . map;
any f xs = foldr (\x t -> ife (f x) True t) False xs;
maybe n j m = case m of { Nothing -> n; Just x -> j x };
lstLookup s = foldr (\h t -> uncurry (\k v -> ife (lstEq s k) (Just v) t) h) Nothing;
data Ast = R String | V String | A Ast Ast | L String Ast;
pure x = \inp -> Just (x, inp);
sat' f = \h t -> ife (f h) (pure h t) Nothing;
sat f inp = flst inp Nothing (sat' f);
bind f m = case m of
{ Nothing -> Nothing
; Just x -> uncurry f x
};
ap x y = \inp -> bind (\a t -> bind (\b u -> pure (a b) u) (y t)) (x inp);
(<*>) = ap;
fmap f x = ap (pure f) x;
(<$>) = fmap;
(>>=) x y = \inp -> bind (\a t -> y a t) (x inp);
(<|>) x y = \inp -> case x inp of
{ Nothing -> y inp
; Just x -> Just x
};
liftA2 f x y = ap (fmap f x) y;
(*>) = liftA2 \x y -> y;
(<*) = liftA2 \x y -> x;
many p = liftA2 (:) p (many p) <|> pure [];
some p = liftA2 (:) p (many p);
sepBy1 p sep = liftA2 (:) p (many (sep *> p));
sepBy p sep = sepBy1 p sep <|> pure [];
char c = sat \x -> x == c;
between x y p = x *> (p <* y);
com = char '-' *> between (char '-') (char '\n') (many (sat \c -> not (c == '\n')));
sp = many ((wrap <$> (sat (\c -> (c == ' ') || (c == '\n')))) <|> com);
spc f = f <* sp;
spch = spc . char;
wantWith pred f inp = bind (sat' pred) (f inp);
want f s inp = wantWith (lstEq s) f inp;
paren = between (spch '(') (spch ')');
small = sat \x -> ((x <= 'z') && ('a' <= x)) || (x == '_');
large = sat \x -> (x <= 'Z') && ('A' <= x);
digit = sat \x -> (x <= '9') && ('0' <= x);
varLex = liftA2 (:) small (many (small <|> large <|> digit <|> char '\''));
conId = spc (liftA2 (:) large (many (small <|> large <|> digit <|> char '\'')));
keyword s = spc (want varLex s);
varId = spc (wantWith (not . lstEq "of") varLex);
opLex = some (sat (\c -> elem c ":!#$%&*+./<=>?@\\^|-~"));
op = spc opLex <|> between (spch '`') (spch '`') varId;
var = varId <|> paren (spc opLex);
lam r = spch '\\' *> liftA2 (flip (foldr L)) (some varId) (char '-' *> (spch '>' *> r));
listify = fmap (foldr (\h t -> A (A (V ":") h) t) (V "[]"));
escChar = char '\\' *> ((sat (\c -> elem c "'\"\\")) <|> ((\c -> '\n') <$> char 'n'));
litOne delim = fmap (\c -> R ('#':wrap c)) (escChar <|> sat (\c -> not (c == delim)));
litInt = R . ('(':) . (++ ")") <$> spc (some digit);
litStr = listify (between (char '"') (spch '"') (many (litOne '"')));
litChar = between (char '\'') (spch '\'') (litOne '\'');
lit = litStr <|> litChar <|> litInt;
sqLst r = listify (between (spch '[') (spch ']') (sepBy r (spch ',')));
alt r = (,) <$> (conId <|> (wrap <$> paren (spch ':' <|> spch ',')) <|> ((:) <$> spch '[' <*> (wrap <$> spch ']'))) <*> (flip (foldr L) <$> many varId <*> (want op "->" *> r));
braceSep f = between (spch '{') (spch '}') (sepBy f (spch ';'));
alts r = braceSep (alt r);
cas' x as = foldl A (V (concatMap (('|':) . fst) as)) (x:map snd as);
cas r = cas' <$> between (keyword "case") (keyword "of") r <*> alts r;
thenComma r = spch ',' *> (((\x y -> A (A (V ",") y) x) <$> r) <|> pure (A (V ",")));
parenExpr r = (&) <$> r <*> (((\v a -> A (V v) a) <$> op) <|> thenComma r <|> pure id);
rightSect r = ((\v a -> L "@" $ A (A (V v) $ V "@") a) <$> (op <|> (wrap <$> spch ','))) <*> r;
section r = paren (parenExpr r <|> rightSect r);
isFree v expr = case expr of
{ R s -> False
; V s -> lstEq s v
; A x y -> isFree v x || isFree v y
; L w t -> not ((lstEq v w) || not (isFree v t))
};
maybeFix s x = (s, ife (isFree s x) (A (V "\\Y") (L s x)) x);
def r = liftA2 maybeFix var (liftA2 (flip (foldr L)) (many varId) (spch '=' *> r));
addLets ls x = foldr (\p t -> uncurry (\name def -> A (L name t) def) p) x ls;
letin r = addLets <$> between (keyword "let") (keyword "in") (braceSep (def r)) <*> r;
atom r = letin r <|> sqLst r <|> section r <|> cas r <|> lam r <|> (paren (spch ',') *> pure (V ",")) <|> fmap V (conId <|> var) <|> lit;
aexp r = fmap (foldl1 A) (some (atom r));
fix f = f (fix f);
data Assoc = NAssoc | LAssoc | RAssoc;
eqAssoc x y = case x of
{ NAssoc -> case y of { NAssoc -> True ; LAssoc -> False ; RAssoc -> False }
; LAssoc -> case y of { NAssoc -> False ; LAssoc -> True ; RAssoc -> False }
; RAssoc -> case y of { NAssoc -> False ; LAssoc -> False ; RAssoc -> True }
};
precOf s precTab = maybe 9 fst (lstLookup s precTab);
assocOf s precTab = maybe LAssoc snd (lstLookup s precTab);
opWithPrec precTab n = wantWith (\s -> n == precOf s precTab) op;
opFold precTab e xs = case xs of
{ [] -> e
; (:) x xt -> case find (\y -> not (eqAssoc (assocOf (fst x) precTab) (assocOf (fst y) precTab))) xt of
{ Nothing -> case assocOf (fst x) precTab of
{ NAssoc -> case xt of
{ [] -> uncurry (\op y -> A (A (V op) e) y) x
; (:) y yt -> undefined
}
; LAssoc -> foldl (\a b -> uncurry (\op y -> A (A (V op) a) y) b) e xs
; RAssoc -> (foldr (\a b -> uncurry (\op y -> \e -> A (A (V op) e) (b y)) a) id xs) e
}
; Just y -> undefined
}
};
expr precTab = fix \r n -> ife (n <= 9) (liftA2 (opFold precTab) (r (succ n)) (many (liftA2 (\a b -> (a,b)) (opWithPrec precTab n) (r (succ n))))) (aexp (r 0));
data Type = TC String | TV String | TAp Type Type;
data Constr = Constr String [Type];
data Adt = Adt Type [Constr];
_type r = foldl1 TAp <$> some r;
typeConstant = (\s -> ife (lstEq "String" s) (TAp (TC "[]") (TC "Int")) (TC s)) <$> conId;
aType = paren ((&) <$> _type aType <*> ((spch ',' *> ((\a b -> TAp (TAp (TC ",") b) a) <$> _type aType)) <|> pure id)) <|> typeConstant <|> (TV <$> varId) <|> (TAp (TC "[]") <$> between (spch '[') (spch ']') (_type aType));
simpleType c vs = foldl TAp (TC c) (map TV vs);
adt = Adt <$> between (keyword "data") (spch '=') (simpleType <$> conId <*> many varId) <*> (sepBy (Constr <$> conId <*> many aType) (spch '|'));
prec = (\c -> ord c - ord '0') <$> spc digit;
fixityList a n os = map (\o -> (o, (n, a))) os;
fixityDecl kw a = between (keyword kw) (spch ';') (fixityList a <$> prec <*> sepBy op (spch ','));
fixity = fixityDecl "infix" NAssoc <|> fixityDecl "infixl" LAssoc <|> fixityDecl "infixr" RAssoc;
arr a b = TAp (TAp (TC "->") a) b;
-- type Program = ([(String, (Type, Ast))], [(String, Ast)])
prims = let
{ ii = arr (TC "Int") (TC "Int")
; iii = arr (TC "Int") ii
; bin s = R $ "``BT`T" ++ s } in
[ ("\\Y", (arr (arr (TV "a") (TV "a")) (TV "a"), R "Y"))
, ("==", (arr (TC "Int") (arr (TC "Int") (TC "Bool")), bin "="))
, ("<=", (arr (TC "Int") (arr (TC "Int") (TC "Bool")), bin "L"))
, ("chr", (ii, R "I"))
, ("ord", (ii, R "I"))
, ("succ", (ii, R "`T`(1)+"))
] ++ map (\s -> (s, (iii, bin s))) ["+", "-", "*", "/", "%"];
conOf con = case con of { Constr s _ -> s };
mkCase t cs = (concatMap (('|':) . conOf) cs,
( arr t $ foldr arr (TV "case") $ map (\c -> case c of { Constr _ ts -> foldr arr (TV "case") ts}) cs
, L "x" $ V "x"));
mkStrs = snd . foldl (\p u -> uncurry (\s l -> ('@':s, s : l)) p) ("@", []);
-- For example, creates `Just = \x a b -> b x`.
scottEncode vs s ts = foldr L (foldl (\a b -> A a (V b)) (V s) ts) (ts ++ vs);
scottConstr t cs c = case c of { Constr s ts -> (s,
( foldr arr t ts
, scottEncode (map conOf cs) s $ mkStrs ts)) };
mkAdtDefs a = case a of { Adt t cs -> mkCase t cs : map (scottConstr t cs) cs };
addAdt = first . (++) . mkAdtDefs;
addDef = second . (:);
tops precTab = foldr ($) ([], []) <$> sepBy (addAdt <$> adt <|> addDef <$> def (expr precTab 0)) (spch ';');
program' = sp *> (((":", (5, RAssoc)):) . concat <$> many fixity) >>= tops;
program = first (prims ++)
. addAdt (Adt (TAp (TC "[]") (TV "a")) [Constr "[]" [], Constr ":" [TV "a", TAp (TC "[]") (TV "a")]])
. addAdt (Adt (TAp (TAp (TC ",") (TV "a")) (TV "b")) [Constr "," [TV "a", TV "b"]])
<$> program';
ifz n = ife (0 == n);
showInt' n = ifz n id ((showInt' (n/10)) . ((:) (chr (48+(n%10)))));
showInt n s = ifz n ('0':) (showInt' n) s;
rank ds v = foldr (\d t -> ife (lstEq v (fst d)) (\n -> ('[':) . showInt n . (']':)) (t . succ)) undefined ds 0;
shows f t = case t of
{ R s -> (s++)
; V v -> f v
; A x y -> ('`':) . shows f x . shows f y
; L w t -> undefined
};
data LC = Ze | Su LC | Pass Ast | La LC | App LC LC;
debruijn n e = case e of
{ R s -> Pass (R s)
; V v -> foldr (\h m -> ife (lstEq h v) Ze (Su m)) (Pass (V v)) n
; A x y -> App (debruijn n x) (debruijn n y)
; L s t -> La (debruijn (s:n) t)
};
data Sem = Defer | Closed Ast | Need Sem | Weak Sem;
ldef = \r y -> case y of
{ Defer -> Need (Closed (A (A (R "S") (R "I")) (R "I")))
; Closed d -> Need (Closed (A (R "T") d))
; Need e -> Need (r (Closed (A (R "S") (R "I"))) e)
; Weak e -> Need (r (Closed (R "T")) e)
};
lclo = \r d y -> case y of
{ Defer -> Need (Closed d)
; Closed dd -> Closed (A d dd)
; Need e -> Need (r (Closed (A (R "B") d)) e)
; Weak e -> Weak (r (Closed d) e)
};
lnee = \r e y -> case y of
{ Defer -> Need (r (r (Closed (R "S")) e) (Closed (R "I")))
; Closed d -> Need (r (Closed (A (R "R") d)) e)
; Need ee -> Need (r (r (Closed (R "S")) e) ee)
; Weak ee -> Need (r (r (Closed (R "C")) e) ee)
};
lwea = \r e y -> case y of
{ Defer -> Need e
; Closed d -> Weak (r e (Closed d))
; Need ee -> Need (r (r (Closed (R "B")) e) ee)
; Weak ee -> Weak (r e ee)
};
babsa x y = case x of
{ Defer -> ldef babsa y
; Closed d -> lclo babsa d y
; Need e -> lnee babsa e y
; Weak e -> lwea babsa e y
};
babs t = case t of
{ Ze -> Defer
; Su x -> Weak (babs x)
; Pass s -> Closed s
; La t -> case babs t of
{ Defer -> Closed (R "I")
; Closed d -> Closed (A (R "K") d)
; Need e -> e
; Weak e -> babsa (Closed (R "K")) e
}
; App x y -> babsa (babs x) (babs y)
};
nolam x = case babs (debruijn [] x) of
{ Defer -> undefined
; Closed d -> d
; Need e -> undefined
; Weak e -> undefined
};
dump tab = foldr (\h t -> shows (rank tab) (nolam (snd h)) (';':t)) "" tab;
asm = dump . uncurry \typed defs -> map (second snd) typed ++ defs;
compile s = maybe "?" fst $ (asm <$> program) s;
apply sub t = case t of
{ TC v -> t
; TV v -> maybe t id $ lstLookup v sub
; TAp a b -> TAp (apply sub a) (apply sub b)
};
(@@) s1 s2 = map (second (apply s1)) s2 ++ s1;
occurs s t = case t of
{ TC v -> False
; TV v -> lstEq s v
; TAp a b -> occurs s a || occurs s b
};
varBind s t = case t of
{ TC v -> Just [(s, t)]
; TV v -> ife (lstEq v s) (Just []) (Just [(s, t)])
; TAp a b -> ife (occurs s t) Nothing (Just [(s, t)])
};
mgu unify t u = case t of
{ TC a -> case u of
{ TC b -> ife (lstEq a b) (Just []) Nothing
; TV b -> varBind b t
; TAp a b -> Nothing
}
; TV a -> varBind a u
; TAp a b -> case u of
{ TC b -> Nothing
; TV b -> varBind b t
; TAp c d -> unify b d (mgu unify a c)
}
};
maybeMap f = maybe Nothing (Just . f);
unify a b = maybe Nothing \s -> maybeMap (@@ s) (mgu unify (apply s a) (apply s b));
--instantiate' :: Type -> Int -> [(String, Type)] -> ((Type, Int), [(String, Type)])
instantiate' t n tab = case t of
{ TC s -> ((t, n), tab)
; TV s -> case lstLookup s tab of
{ Nothing -> let { va = TV (s ++ '_':showInt n "") } in ((va, n + 1), (s, va):tab)
; Just v -> ((v, n), tab)
}
; TAp x y ->
fpair (instantiate' x n tab) \tn1 tab1 ->
fpair tn1 \t1 n1 -> fpair (instantiate' y n1 tab1) \tn2 tab2 ->
fpair tn2 \t2 n2 -> ((TAp t1 t2, n2), tab2)
};
--instantiate :: Type -> Int -> (Type, Int)
instantiate t n = fst (instantiate' t n []);
--type SymTab = [(String, (Type, Ast))];
--type Subst = [(String, Type)];
--infer' :: SymTab -> Subst -> Ast -> (Maybe Subst, Int) -> (Type, (Maybe Subst, Int))
infer' typed loc ast = uncurry \cs n ->
let { va = TV ('_':showInt n "") } in case ast of
{ R s -> (TC "Int", (cs, n))
; V s -> maybe
(maybe undefined (\ta -> second (cs,) (instantiate (fst ta) n)) (lstLookup s typed))
(, (cs, n))
(lstLookup s loc)
; A x y ->
fpair (infer' typed loc x (cs, n + 1)) \tx csn1 ->
fpair (infer' typed loc y csn1) \ty csn2 ->
(va, first (unify tx (arr ty va)) csn2)
; L s x -> first (TAp (TAp (TC "->") va)) (infer' typed ((s, va):loc) x (cs, n + 1))
};
apSub = uncurry \ty -> uncurry \ms _ -> maybeMap (flip apply ty) ms;
data Either a b = Left a | Right b;
inferDefs typed defs = flst defs (Right typed) \def rest -> fpair def \s expr ->
case apSub (infer' typed [] expr (Just [], 0)) of
{ Nothing -> Left ("bad type: " ++ s)
; Just t -> inferDefs ((s, (t, expr)) : typed) rest
};
infer = uncurry inferDefs;
showType t = case t of
{ TC s -> s
; TV s -> s
; TAp a b -> concat ["(", showType a, " ", showType b, ")"]
};
dumpTypes s = maybe "parse error" (uncurry \prog rest -> case infer prog of
{ Left err -> err
; Right typed -> concatMap (uncurry \s ta -> s ++ " :: " ++ showType (fst ta) ++ "\n") typed
}) (program s);
typedCompile s = maybe "parse error" (uncurry \prog rest -> case infer prog of
{ Left err -> err
; Right _ -> asm prog
}) (program s);
Compilng this code takes (very roughly) three times as much time and memory to than its predecessor, which perhaps is reasonable as the source is substantially longer and we chose several slow algorithms for the sake of simplicity.
However, this compiler takes about eight times more time and space to build its successor.
The new type checking phase certainly deserves blame, as does the even larger
size of the next compiler. But there is a subtler source of drag. More syntax
sugar; more problems. While functions such as ($) let us reduce clutter in
our code, our bracket abstraction routine sees it as an opaque symbol,
hampering optimization. Laziness helps somewhat: we find ($) compiles to the
I combinator, and the first time the VM reduces something like Ifx it
replaces all references to it with fx.
This is too little too late. As bracket abstraction fails to recognize ($) is
the identity, it adds superfluous combinators. For example:
\x y -> f x $ g y
becomes:
R g(B B(B ($) f))
when it should just be:
R g(B B f)
Classy
In the worst case, types are a burden, and force us to wrestle with the compiler. We twist our code this way and that, and add eye-watering type annotations until it finally compiles.
In contrast, well-designed types do more with less. Haskell’s type system not only enables easy type inference, but also enables typeclasses, a syntax sugar for principled overloading. By bestowing Prolog-like powers to the type checker, the compiler can predictably generate tedious code so humans can ignore irrelevant details.
Again, Typing Haskell in Haskell provides some background. Since we’re generating code as well as checking types, we also need techniques described in John Peterson and Mark Jones, Implementing Type Classes.
We choose the dictionary approach. A dictionary is a record of functions that
is implicitly passed around. For example, if we infer the function foo has
type:
foo :: Eq a => Show a => a -> String
then we may imagine our compiler turning fat arrows into thin arrows:
foo :: Eq a -> Show a -> a -> String
Our compiler then seeks dictionaries that fit the two new arguments of types
Eq a and Show a, and inserts them into the syntax tree.
With this in mind, we modify the type inference functions so they return a
syntax tree along with its type. Most of the time, they just return the input
syntax tree unchanged, but if type constraints are inferred, then we create a
Proof node for each constraint, and apply the syntax tree to these new nodes.
In our example, if t is the syntax tree of foo, then our type inference
function would change it to A (A t (Proof "Eq a")) (Proof "Show a").
Here, we’re using strings to represent constraints for legibiity; in reality,
we have a dedicated data type to hold constraints, though later on, we
do in fact turn them into strings when generating variable names.
We call such a node a Proof because it’s a cute short word, and we think of a
dictionary as proof that a certain constraint is satisfied. Peterson and Jones
instead write "Placeholder".
Typeclass methods are included in the above. For example, while processing the expression:
(==) (2+2) 5
we infer that (==) has type Eq a ⇒ a → a → Bool, so we modify the
syntax tree to:
(select-==) (Proof "Eq a") (2+2) 5
After type unification, we learn a is Int:
(select-==) (Proof "Eq Int") (2+2) 5
The next phase constructs records of functions to be used as proofs. We loosely follow 'Typing Haskell in Haskell' once more, and search for instances that match a given constraint. A matching instance may create more constraints.
We walk through how our compiler finds a proof for:
Proof "Eq [[Int]]"
Our compiler finds an instance match: Eq a ⇒ Eq [a], so it rewrites the
above as:
(V "Eq [a]") (Proof "Eq [Int]")
The "Eq [a]" string is taken verbatim from an instance declaration, while the "Eq [Int]" is the result of a type substitution found during unification on "Eq a".
Our compiler recursively seeks an instance match for the new Proof. Again it
finds Eq a ⇒ Eq [a], so the next rewrite yields:
(V "Eq [a]") ((V "Eq [a]") (Proof "Eq Int"))
and again it recursively looks for an instance match. It finds the Eq Int
instance, and we have:
(V "Eq [a]") ((V "Eq [a]") (V "Eq Int"))
This works, because our compiler has previously processed all class and
instance declarations, and has prepared the symbol table to map "Eq Int"
to a record of functions for integer equality testing, and "Eq [a]" to a
function that takes a "Eq a" and returns a record of functions for equality
testing on lists of type a.
Overloading complicates our handling of recursion. For example,
each occurrence of (==) in:
instance Eq (Int, String) where (x, y) == (z, w) = x == z && y == w
refers to a distinct function, so introducing the Y combinator here is
incorrect. We should only look for recursion after type inference expands
them to select-== Dict-Eq-Int and select-== Dict-Eq-String, and we
look for recursion at the level of dictionaries.
Among the many deficiencies in our compiler: we lack support for class contexts; our code allows instances to stomp over one another; our algorithm for finding proofs may not terminate.
Without garbage collection, this compiler requires unreasonable amounts of memory.
------------------------------------------------------------------------
-- Type classes.
------------------------------------------------------------------------
infixr 9 .;
infixr 5 ++;
infixl 4 <*> , <$> , <* , *>;
infixl 3 <|>;
infixr 0 $;
undefined = undefined;
($) f x = f x;
id x = x;
flip f x y = f y x;
(&) x f = f x;
data Bool = True | False;
data Maybe a = Nothing | Just a;
fpair p = \f -> case p of { (,) x y -> f x y };
fst p = case p of { (,) x y -> x };
snd p = case p of { (,) x y -> y };
first f p = fpair p \x y -> (f x, y);
second f p = fpair p \x y -> (x, f y);
ife a b c = case a of { True -> b ; False -> c };
not a = case a of { True -> False; False -> True };
(.) f g x = f (g x);
(||) f g = ife f True g;
(&&) f g = ife f g False;
flst xs n c = case xs of { [] -> n; (:) h t -> c h t };
lstEq xs ys = case xs of
{ [] -> flst ys True (\h t -> False)
; (:) x xt -> flst ys False (\y yt -> ife (x == y) (lstEq xt yt) False)
};
maybe n j m = case m of { Nothing -> n; Just x -> j x };
foldr c n l = flst l n (\h t -> c h(foldr c n t));
foldr1 c l = maybe undefined id (flst l undefined (\h t -> foldr (\x m -> Just (case m of { Nothing -> x ; Just y -> c x y })) Nothing l));
foldl = \f a bs -> foldr (\b g x -> g (f x b)) (\x -> x) bs a;
foldl1 f bs = flst bs undefined (\h t -> foldl f h t);
elem k xs = foldr (\x t -> ife (x == k) True t) False xs;
find f xs = foldr (\x t -> ife (f x) (Just x) t) Nothing xs;
(++) = flip (foldr (:));
concat = foldr (++) [];
wrap c = c:[];
map = flip (foldr . ((:) .)) [];
concatMap = (concat .) . map;
fmaybe m n j = case m of { Nothing -> n; Just x -> j x };
lookupWith eq s = foldr (\h t -> fpair h (\k v -> ife (eq s k) (Just v) t)) Nothing;
lstLookup = lookupWith lstEq;
data Type = TC String | TV String | TAp Type Type;
data Ast = R String | V String | A Ast Ast | L String Ast | Proof Pred;
pure x = \inp -> Just (x, inp);
sat' f = \h t -> ife (f h) (pure h t) Nothing;
sat f inp = flst inp Nothing (sat' f);
bind f m = case m of
{ Nothing -> Nothing
; Just x -> fpair x f
};
ap x y = \inp -> bind (\a t -> bind (\b u -> pure (a b) u) (y t)) (x inp);
(<*>) = ap;
fmap f x = ap (pure f) x;
(<$>) = fmap;
(>>=) x y = \inp -> bind (\a t -> y a t) (x inp);
(<|>) x y = \inp -> case x inp of
{ Nothing -> y inp
; Just x -> Just x
};
liftA2 f x y = ap (fmap f x) y;
(*>) = liftA2 \x y -> y;
(<*) = liftA2 \x y -> x;
many p = liftA2 (:) p (many p) <|> pure [];
some p = liftA2 (:) p (many p);
sepBy1 p sep = liftA2 (:) p (many (sep *> p));
sepBy p sep = sepBy1 p sep <|> pure [];
char c = sat \x -> x == c;
between x y p = x *> (p <* y);
com = char '-' *> between (char '-') (char '\n') (many (sat \c -> not (c == '\n')));
sp = many ((wrap <$> (sat (\c -> (c == ' ') || (c == '\n')))) <|> com);
spc f = f <* sp;
spch = spc . char;
wantWith pred f inp = bind (sat' pred) (f inp);
want f s inp = wantWith (lstEq s) f inp;
paren = between (spch '(') (spch ')');
small = sat \x -> ((x <= 'z') && ('a' <= x)) || (x == '_');
large = sat \x -> (x <= 'Z') && ('A' <= x);
digit = sat \x -> (x <= '9') && ('0' <= x);
varLex = liftA2 (:) small (many (small <|> large <|> digit <|> char '\''));
conId = spc (liftA2 (:) large (many (small <|> large <|> digit <|> char '\'')));
keyword s = spc (want varLex s);
varId = spc (wantWith (\s -> not (lstEq "of" s || lstEq "where" s)) varLex);
opLex = some (sat (\c -> elem c ":!#$%&*+./<=>?@\\^|-~"));
op = spc opLex <|> between (spch '`') (spch '`') varId;
var = varId <|> paren (spc opLex);
lam r = spch '\\' *> liftA2 (flip (foldr L)) (some varId) (char '-' *> (spch '>' *> r));
listify = fmap (foldr (\h t -> A (A (V ":") h) t) (V "[]"));
escChar = char '\\' *> ((sat (\c -> elem c "'\"\\")) <|> ((\c -> '\n') <$> char 'n'));
litOne delim = fmap (\c -> R ('#':wrap c)) (escChar <|> sat (\c -> not (c == delim)));
litInt = R . ('(':) . (++ ")") <$> spc (some digit);
litStr = listify (between (char '"') (spch '"') (many (litOne '"')));
litChar = between (char '\'') (spch '\'') (litOne '\'');
lit = litStr <|> litChar <|> litInt;
sqLst r = listify (between (spch '[') (spch ']') (sepBy r (spch ',')));
alt r = (,) <$> (conId <|> (wrap <$> paren (spch ':' <|> spch ',')) <|> ((:) <$> spch '[' <*> (wrap <$> spch ']'))) <*> (flip (foldr L) <$> many varId <*> (want op "->" *> r));
braceSep f = between (spch '{') (spch '}') (sepBy f (spch ';'));
alts r = braceSep (alt r);
cas' x as = foldl A (V (concatMap (('|':) . fst) as)) (x:map snd as);
cas r = cas' <$> between (keyword "case") (keyword "of") r <*> alts r;
thenComma r = spch ',' *> (((\x y -> A (A (V ",") y) x) <$> r) <|> pure (A (V ",")));
parenExpr r = (&) <$> r <*> (((\v a -> A (V v) a) <$> op) <|> thenComma r <|> pure id);
rightSect r = ((\v a -> L "@" $ A (A (V v) $ V "@") a) <$> (op <|> (wrap <$> spch ','))) <*> r;
section r = paren (parenExpr r <|> rightSect r);
isFree v expr = case expr of
{ R s -> False
; V s -> lstEq s v
; A x y -> isFree v x || isFree v y
; L w t -> not ((lstEq v w) || not (isFree v t))
; Proof _ -> False
};
maybeFix s x = ife (isFree s x) (A (V "\\Y") (L s x)) x;
def r = liftA2 (,) var (liftA2 (flip (foldr L)) (many varId) (spch '=' *> r));
addLets ls x = foldr (\p t -> fpair p (\name def -> A (L name t) $ maybeFix name def)) x ls;
letin r = addLets <$> between (keyword "let") (keyword "in") (braceSep (def r)) <*> r;
atom r = letin r <|> sqLst r <|> section r <|> cas r <|> lam r <|> (paren (spch ',') *> pure (V ",")) <|> fmap V (conId <|> var) <|> lit;
aexp r = fmap (foldl1 A) (some (atom r));
fix f = f (fix f);
data Assoc = NAssoc | LAssoc | RAssoc;
eqAssoc x y = case x of
{ NAssoc -> case y of { NAssoc -> True ; LAssoc -> False ; RAssoc -> False }
; LAssoc -> case y of { NAssoc -> False ; LAssoc -> True ; RAssoc -> False }
; RAssoc -> case y of { NAssoc -> False ; LAssoc -> False ; RAssoc -> True }
};
precOf s precTab = maybe 9 fst (lstLookup s precTab);
assocOf s precTab = maybe LAssoc snd (lstLookup s precTab);
opWithPrec precTab n = wantWith (\s -> n == precOf s precTab) op;
opFold precTab e xs = case xs of
{ [] -> e
; (:) x xt -> case find (\y -> not (eqAssoc (assocOf (fst x) precTab) (assocOf (fst y) precTab))) xt of
{ Nothing -> case assocOf (fst x) precTab of
{ NAssoc -> case xt of
{ [] -> fpair x (\op y -> A (A (V op) e) y)
; (:) y yt -> undefined
}
; LAssoc -> foldl (\a b -> fpair b (\op y -> A (A (V op) a) y)) e xs
; RAssoc -> (foldr (\a b -> fpair a (\op y -> \e -> A (A (V op) e) (b y))) id xs) e
}
; Just y -> undefined
}
};
expr precTab = fix \r n -> ife (n <= 9) (liftA2 (opFold precTab) (r (succ n)) (many (liftA2 (\a b -> (a,b)) (opWithPrec precTab n) (r (succ n))))) (aexp (r 0));
data Constr = Constr String [Type];
data Pred = Pred String Type;
data Qual = Qual [Pred] Type;
data Top = Adt Type [Constr] | Def (String, Ast) | Class String Type [(String, Type)] | Inst String Qual [(String, Ast)];
arr a b = TAp (TAp (TC "->") a) b;
bType r = foldl1 TAp <$> some r;
_type r = foldr1 arr <$> sepBy (bType r) (spc (want opLex "->"));
typeConstant = (\s -> ife (lstEq "String" s) (TAp (TC "[]") (TC "Int")) (TC s)) <$> conId;
aType = paren ((&) <$> _type aType <*> ((spch ',' *> ((\a b -> TAp (TAp (TC ",") b) a) <$> _type aType)) <|> pure id)) <|>
typeConstant <|> (TV <$> varId) <|>
(spch '[' *> (spch ']' *> pure (TC "[]") <|> TAp (TC "[]") <$> (_type aType <* spch ']')));
simpleType c vs = foldl TAp (TC c) (map TV vs);
adt = Adt <$> between (keyword "data") (spch '=') (simpleType <$> conId <*> many varId) <*> (sepBy (Constr <$> conId <*> many aType) (spch '|'));
prec = (\c -> ord c - ord '0') <$> spc digit;
fixityList a n os = map (\o -> (o, (n, a))) os;
fixityDecl kw a = between (keyword kw) (spch ';') (fixityList a <$> prec <*> sepBy op (spch ','));
fixity = fixityDecl "infix" NAssoc <|> fixityDecl "infixl" LAssoc <|> fixityDecl "infixr" RAssoc;
noQual = Qual [];
genDecl = (,) <$> var <*> (char ':' *> spch ':' *> _type aType);
classDecl = keyword "class" *> (Class <$> conId <*> (TV <$> varId) <*> (keyword "where" *> braceSep genDecl));
inst = _type aType;
instDecl r = keyword "instance" *>
((\ps cl ty defs -> Inst cl (Qual ps ty) defs) <$>
(((wrap .) . Pred <$> conId <*> (inst <* want op "=>")) <|> pure [])
<*> conId <*> inst <*> (keyword "where" *> braceSep (def r)));
tops precTab = sepBy
( adt
<|> Def <$> def (expr precTab 0)
<|> classDecl
<|> instDecl (expr precTab 0)
) (spch ';');
program' = sp *> (((":", (5, RAssoc)):) . concat <$> many fixity) >>= tops;
eqPre = fmaybe (program' $ "class Eq a where { (==) :: a -> a -> Bool };\n" ++
"instance Eq Int where { (==) = intEq };\n") undefined fst;
ordPre = fmaybe (program' $ "class Ord a where { (<=) :: a -> a -> Bool };\n" ++
"instance Ord Int where { (<=) = intLE };\n") undefined fst;
program = (
(eqPre ++ ordPre ++
[ Adt (TAp (TC "[]") (TV "a")) [Constr "[]" [], Constr ":" [TV "a", TAp (TC "[]") (TV "a")]]
, Adt (TAp (TAp (TC ",") (TV "a")) (TV "b")) [Constr "," [TV "a", TV "b"]]]) ++) <$> program';
prims = let
{ ii = arr (TC "Int") (TC "Int")
; iii = arr (TC "Int") ii
; bin s = R $ "``BT`T" ++ s } in map (second (first noQual)) $
[ ("\\Y", (arr (arr (TV "a") (TV "a")) (TV "a"), R "Y"))
, ("intEq", (arr (TC "Int") (arr (TC "Int") (TC "Bool")), bin "="))
, ("intLE", (arr (TC "Int") (arr (TC "Int") (TC "Bool")), bin "L"))
, ("chr", (ii, R "I"))
, ("ord", (ii, R "I"))
, ("succ", (ii, R "`T`(1)+"))
] ++ map (\s -> (s, (iii, bin s))) ["+", "-", "*", "/", "%"];
ifz n = ife (0 == n);
showInt' n = ifz n id ((showInt' (n/10)) . ((:) (chr (48+(n%10)))));
showInt n s = ifz n ('0':) (showInt' n) s;
rank ds v = foldr (\d t -> ife (lstEq v (fst d)) (\n -> ('[':) . showInt n . (']':)) (t . succ)) undefined ds 0;
shows f t = case t of
{ R s -> (s++)
; V v -> f v
; A x y -> ('`':) . shows f x . shows f y
; L w t -> undefined
; Proof _ -> undefined
};
data LC = Ze | Su LC | Pass Ast | La LC | App LC LC;
debruijn n e = case e of
{ R s -> Pass (R s)
; V v -> foldr (\h m -> ife (lstEq h v) Ze (Su m)) (Pass (V v)) n
; A x y -> App (debruijn n x) (debruijn n y)
; L s t -> La (debruijn (s:n) t)
; Proof _ -> undefined
};
data Sem = Defer | Closed Ast | Need Sem | Weak Sem;
ldef = \r y -> case y of
{ Defer -> Need (Closed (A (A (R "S") (R "I")) (R "I")))
; Closed d -> Need (Closed (A (R "T") d))
; Need e -> Need (r (Closed (A (R "S") (R "I"))) e)
; Weak e -> Need (r (Closed (R "T")) e)
};
lclo = \r d y -> case y of
{ Defer -> Need (Closed d)
; Closed dd -> Closed (A d dd)
; Need e -> Need (r (Closed (A (R "B") d)) e)
; Weak e -> Weak (r (Closed d) e)
};
lnee = \r e y -> case y of
{ Defer -> Need (r (r (Closed (R "S")) e) (Closed (R "I")))
; Closed d -> Need (r (Closed (A (R "R") d)) e)
; Need ee -> Need (r (r (Closed (R "S")) e) ee)
; Weak ee -> Need (r (r (Closed (R "C")) e) ee)
};
lwea = \r e y -> case y of
{ Defer -> Need e
; Closed d -> Weak (r e (Closed d))
; Need ee -> Need (r (r (Closed (R "B")) e) ee)
; Weak ee -> Weak (r e ee)
};
babsa x y = case x of
{ Defer -> ldef babsa y
; Closed d -> lclo babsa d y
; Need e -> lnee babsa e y
; Weak e -> lwea babsa e y
};
babs t = case t of
{ Ze -> Defer
; Su x -> Weak (babs x)
; Pass s -> Closed s
; La t -> case babs t of
{ Defer -> Closed (R "I")
; Closed d -> Closed (A (R "K") d)
; Need e -> e
; Weak e -> babsa (Closed (R "K")) e
}
; App x y -> babsa (babs x) (babs y)
};
nolam x = case babs (debruijn [] x) of
{ Defer -> undefined
; Closed d -> d
; Need e -> undefined
; Weak e -> undefined
};
asm tab = foldr (\h t -> shows (rank tab) (nolam (snd h)) (';':t)) "" tab;
apply sub t = case t of
{ TC v -> t
; TV v -> fmaybe (lstLookup v sub) t id
; TAp a b -> TAp (apply sub a) (apply sub b)
};
(@@) s1 s2 = map (second (apply s1)) s2 ++ s1;
occurs s t = case t of
{ TC v -> False
; TV v -> lstEq s v
; TAp a b -> occurs s a || occurs s b
};
varBind s t = case t of
{ TC v -> Just [(s, t)]
; TV v -> ife (lstEq v s) (Just []) (Just [(s, t)])
; TAp a b -> ife (occurs s t) Nothing (Just [(s, t)])
};
mgu unify t u = case t of
{ TC a -> case u of
{ TC b -> ife (lstEq a b) (Just []) Nothing
; TV b -> varBind b t
; TAp a b -> Nothing
}
; TV a -> varBind a u
; TAp a b -> case u of
{ TC b -> Nothing
; TV b -> varBind b t
; TAp c d -> unify b d (mgu unify a c)
}
};
maybeMap f = maybe Nothing (Just . f);
unify a b = maybe Nothing \s -> maybeMap (@@ s) (mgu unify (apply s a) (apply s b));
--instantiate' :: Type -> Int -> [(String, Type)] -> ((Type, Int), [(String, Type)])
instantiate' t n tab = case t of
{ TC s -> ((t, n), tab)
; TV s -> case lstLookup s tab of
{ Nothing -> let { va = TV (showInt n "") } in ((va, n + 1), (s, va):tab)
; Just v -> ((v, n), tab)
}
; TAp x y ->
fpair (instantiate' x n tab) \tn1 tab1 ->
fpair tn1 \t1 n1 -> fpair (instantiate' y n1 tab1) \tn2 tab2 ->
fpair tn2 \t2 n2 -> ((TAp t1 t2, n2), tab2)
};
instantiatePred pred xyz = case pred of { Pred s t -> fpair xyz \xy tab -> fpair xy \out n -> first (first ((:out) . Pred s)) (instantiate' t n tab) };
--instantiate :: Qual -> Int -> (Qual, Int)
instantiate qt n = case qt of { Qual ps t ->
fpair (foldr instantiatePred (([], n), []) ps) \xy tab -> fpair xy \ps1 n1 ->
first (Qual ps1) (fst (instantiate' t n1 tab))
};
--type SymTab = [(String, (Qual, Ast))];
--type Subst = [(String, Type)];
--infer' :: SymTab -> Subst -> Ast -> (Maybe Subst, Int) -> ((Type, Ast), (Maybe Subst, Int))
infer' typed loc ast csn = fpair csn \cs n ->
let { va = TV (showInt n "") } in case ast of
{ R s -> ((TC "Int", ast), csn)
; V s -> fmaybe (lstLookup s loc)
(fmaybe (lstLookup s typed) undefined
\ta -> fpair (instantiate (fst ta) n) \q n1 -> case q of { Qual preds ty -> ((ty, foldl A ast (map Proof preds)), (cs, n1)) })
((, csn) . (, ast))
; A x y ->
fpair (infer' typed loc x (cs, n + 1)) \tax csn1 -> fpair tax \tx ax ->
fpair (infer' typed loc y csn1) \tay csn2 -> fpair tay \ty ay ->
((va, A ax ay), first (unify tx (arr ty va)) csn2)
; L s x -> first (\ta -> fpair ta \t a -> (arr va t, L s a)) (infer' typed ((s, va):loc) x (cs, n + 1))
; Proof _ -> undefined
};
onType f pred = case pred of { Pred s t -> Pred s (f t) };
typeEq t u = case t of
{ TC s -> case u of
{ TC t -> lstEq t s
; TV _ -> False
; TAp _ _ -> False
}
; TV s -> case u of
{ TC _ -> False
; TV t -> lstEq t s
; TAp _ _ -> False
}
; TAp a b -> case u of
{ TC _ -> False
; TV _ -> False
; TAp c d -> typeEq a c && typeEq b d
}
};
predEq p q = case p of { Pred s a -> case q of { Pred t b ->
lstEq s t && typeEq a b }};
predApply sub p = onType (apply sub) p;
all f = foldr (&&) True . map f;
filter f = foldr (\x xs ->ife (f x) (x:xs) xs) [];
intersect xs ys = filter (\x -> fmaybe (find (lstEq x) ys) False (\_ -> True)) xs;
merge s1 s2 = ife (all (\v -> typeEq (apply s1 $ TV v) (apply s2 $ TV v))
$ map fst s1 `intersect` map fst s2) (Just $ s1 ++ s2) Nothing;
match h t = case h of
{ TC a -> case t of
{ TC b -> ife (lstEq a b) (Just []) Nothing
; TV b -> Nothing
; TAp a b -> Nothing
}
; TV a -> Just [(a, t)]
; TAp a b -> case t of
{ TC b -> Nothing
; TV b -> Nothing
; TAp c d -> case match a c of
{ Nothing -> Nothing
; Just ac -> case match b d of
{ Nothing -> Nothing
; Just bd -> merge ac bd
}
}
}
};
matchPred h p = case p of { Pred _ t -> match h t };
showType t = case t of
{ TC s -> s
; TV s -> s
; TAp a b -> concat ["(", showType a, " ", showType b, ")"]
};
showPred p = case p of { Pred s t -> s ++ (' ':showType t) ++ " => "};
findInst r qn p insts = case insts of
{ [] ->
fpair qn \q n -> let { v = '*':showInt n "" } in (((p, v):q, n + 1), V v)
; (:) i is -> case i of { Qual ps h -> case matchPred h p of
{ Nothing -> findInst r qn p is
; Just u -> foldl (\qnt p -> fpair qnt \qn1 t -> second (A t)
(r (predApply u p) qn1)) (qn, V (case p of { Pred s _ -> showPred $ Pred s h})) ps
}}};
findProof is pred psn = fpair psn \ps n -> case lookupWith predEq pred ps of
{ Nothing -> case pred of { Pred s t -> case lstLookup s is of
{ Nothing -> undefined -- No instances!
; Just insts -> findInst (findProof is) psn pred insts
}}
; Just s -> (psn, V s)
};
prove' ienv sub psn a = case a of
{ R _ -> (psn, a)
; V _ -> (psn, a)
; A x y -> let { p1 = prove' ienv sub psn x } in fpair p1 \psn1 x1 ->
second (A x1) (prove' ienv sub psn1 y)
; L s t -> second (L s) (prove' ienv sub psn t)
; Proof raw -> findProof ienv (predApply sub raw) psn
};
--prove :: [(String, [Qual])] -> (Type, Ast) -> Subst -> (Qual, Ast)
prove ienv ta sub = fpair ta \t a ->
fpair (prove' ienv sub ([], 0) a) \psn x -> fpair psn \ps _ ->
(Qual (map fst ps) (apply sub t), foldr L x (map snd ps));
data Either a b = Left a | Right b;
dictVars ps n = flst ps ([], n) \p pt -> first ((p, '*':showInt n ""):) (dictVars pt $ n + 1);
-- qi = Qual of instance, e.g. Eq t => [t] -> [t] -> Bool
inferMethod ienv typed qi def = fpair def \s expr ->
fpair (infer' typed [] expr (Just [], 0)) \ta msn ->
case lstLookup s typed of
{ Nothing -> undefined -- No such method.
-- e.g. qac = Eq a => a -> a -> Bool, some AST (product of single method)
; Just qac -> fpair msn \ms n -> case ms of
{ Nothing -> undefined -- Type check fails.
; Just sub -> fpair (instantiate (fst qac) n) \q1 n1 -> case q1 of { Qual psc tc -> case psc of
{ [] -> undefined -- Unreachable.
; (:) headPred shouldBeNull -> case qi of { Qual psi ti ->
case headPred of { Pred _ headT -> case match headT ti of
{ Nothing -> undefined
-- e.g. Eq t => [t] -> [t] -> Bool
-- instantiate and match it against type of ta
; Just subc ->
fpair (instantiate (Qual psi $ apply subc tc) n1) \q2 n2 ->
case q2 of { Qual ps2 t2 -> fpair ta \tx ax ->
case match (apply sub tx) t2 of
{ Nothing -> undefined -- Class/instance type conflict.
; Just subx -> snd $ prove' ienv (subx @@ sub) (dictVars ps2 0) ax
}}}}}}}}};
inferInst ienv typed inst = fpair inst \cl qds -> fpair qds \q ds ->
case q of { Qual ps t -> let { s = showPred $ Pred cl t } in
(s, (,) (noQual $ TC "DICT") $ maybeFix s $ foldr L (L "@" $ foldl A (V "@") (map (inferMethod ienv typed q) ds)) (map snd $ fst $ dictVars ps 0))
};
reverse = foldl (flip (:)) [];
inferDefs ienv defs typed = flst defs (Right $ reverse typed) \edef rest -> case edef of
{ Left def -> fpair def \s expr -> fpair (infer' typed [] (maybeFix s expr) (Just [], 0)) \ta msn ->
fpair msn \ms _ -> case maybeMap (prove ienv ta) ms of
{ Nothing -> Left ("bad type: " ++ s)
; Just qa -> inferDefs ienv rest ((s, qa):typed)
}
; Right inst -> inferDefs ienv rest (inferInst ienv typed inst:typed)
};
conOf con = case con of { Constr s _ -> s };
mkCase t cs = (concatMap (('|':) . conOf) cs,
( noQual $ arr t $ foldr arr (TV "case") $ map (\c -> case c of { Constr _ ts -> foldr arr (TV "case") ts}) cs
, L "x" $ V "x"));
mkStrs = snd . foldl (\p u -> fpair p (\s l -> ('@':s, s : l))) ("@", []);
-- For example, creates `Just = \x a b -> b x`.
scottEncode vs s ts = foldr L (foldl (\a b -> A a (V b)) (V s) ts) (ts ++ vs);
scottConstr t cs c = case c of { Constr s ts -> (s,
( noQual $ foldr arr t ts
, scottEncode (map conOf cs) s $ mkStrs ts)) };
mkAdtDefs t cs = mkCase t cs : map (scottConstr t cs) cs;
-- * instance environment
-- * definitions, including those of instances
-- * Typed ASTs, ready for compilation, including ADTs and methods,
-- e.g. (==), (Eq a => a -> a -> Bool, select-==)
data Neat = Neat [(String, [Qual])] [Either (String, Ast) (String, (Qual, [(String, Ast)]))] [(String, (Qual, Ast))];
fneat neat f = case neat of { Neat a b c -> f a b c };
select f xs acc = flst xs (Nothing, acc) \x xt -> ife (f x) (Just x, xt ++ acc) (select f xt (x:acc));
addInstance s q is = fpair (select (\kv -> lstEq s (fst kv)) is []) \m xs -> case m of
{ Nothing -> (s, [q]):xs
; Just sqs -> second (q:) sqs:xs
};
mkSel ms s = L "*" $ A (V "*") $ foldr L (V $ '*':s) $ map (('*':) . fst) ms;
untangle = foldr (\top acc -> fneat acc \ienv fs typed -> case top of
{ Adt t cs -> Neat ienv fs (mkAdtDefs t cs ++ typed)
; Def f -> Neat ienv (Left f : fs) typed
; Class classId v ms -> Neat ienv fs (
map (\st -> fpair st \s t -> (s, (Qual [Pred classId v] t, mkSel ms s))) ms
++ typed)
; Inst cl q ds -> Neat (addInstance cl q ienv) (Right (cl, (q, ds)):fs) typed
}) (Neat [] [] prims);
infer prog = fneat (untangle prog) inferDefs;
showQual q = case q of { Qual ps t -> concatMap showPred ps ++ showType t };
dumpTypes s = fmaybe (program s) "parse error" \progRest ->
fpair progRest \prog rest -> case infer prog of
{ Left err -> err
; Right typed -> concatMap (\p -> fpair p \s qa -> s ++ " :: " ++ showQual (fst qa) ++ "\n") typed
};
compile s = fmaybe (program s) "parse error" \progRest ->
fpair progRest \prog rest -> case infer prog of
{ Left err -> err
; Right qas -> asm $ map (second snd) qas
};
Barely
Our compilers are becoming noticeably slower. The main culprit is the type unification algorithm we copied from the paper. It is elegant and simple, but also grossly inefficient. The pain is exacerbated by long string constants, which expand to a chain of cons calls before type checking.
Fortunately, we can easily defer expansion so it takes place after type checking. This alleviates enough of the suffering that we’ll leave improving unification for another time.
This change is a good opportunity to tidy up. In particular, we eliminate the
murky handling of the R data constructor: before type checking, it
represented integer constants, while after type checking, its field was to be
passed verbatim to the next phase. Now, data types clear up the picture.
We immediately take advantage of the neater code and add a few rewrite rules to cut down the number of combinators.
To make this incarnation of our compiler more substantial, we knuckle down
and implement a Map based on
Adams
trees. Again, we mostly copy code from a paper. The running time improves
slightly after replacing the association list used in the last compilation
step with Map.
We choose the BB-2.5 variant, based on the benchmarks in the paper, though
it is troubling that Data.Map chose BB-3 trees.
We also move the assembler from C to Haskell, that is, our compiler now outputs bare machine code rather than ION assembly.
-- Output bare memory dump instead of ION assembly.
infixr 9 .;
infixl 7 *;
infixl 6 + , -;
infixr 5 ++;
infixl 4 <*> , <$> , <* , *>;
infix 4 == , <=;
infixl 3 && , <|>;
infixl 2 ||;
infixr 0 $;
class Eq a where { (==) :: a -> a -> Bool };
instance Eq Int where { (==) = intEq };
undefined = undefined;
($) f x = f x;
id x = x;
flip f x y = f y x;
(&) x f = f x;
data Bool = True | False;
class Ord a where { (<=) :: a -> a -> Bool };
instance Ord Int where { (<=) = intLE };
data Ordering = LT | GT | EQ;
compare x y = case x <= y of
{ True -> case y <= x of
{ True -> EQ
; False -> LT
}
; False -> GT
};
instance Ord a => Ord [a] where {
(<=) xs ys = case xs of
{ [] -> True
; (:) x xt -> case ys of
{ [] -> False
; (:) y yt -> case compare x y of
{ LT -> True
; GT -> False
; EQ -> xt <= yt
}
}
}
};
data Maybe a = Nothing | Just a;
fpair p = \f -> case p of { (,) x y -> f x y };
fst p = case p of { (,) x y -> x };
snd p = case p of { (,) x y -> y };
first f p = fpair p \x y -> (f x, y);
second f p = fpair p \x y -> (x, f y);
ife a b c = case a of { True -> b ; False -> c };
not a = case a of { True -> False; False -> True };
(.) f g x = f (g x);
(||) f g = ife f True g;
(&&) f g = ife f g False;
flst xs n c = case xs of { [] -> n; (:) h t -> c h t };
instance Eq a => Eq [a] where { (==) xs ys = case xs of
{ [] -> case ys of
{ [] -> True
; (:) _ _ -> False
}
; (:) x xt -> case ys of
{ [] -> False
; (:) y yt -> x == y && xt == yt
}
}};
maybe n j m = case m of { Nothing -> n; Just x -> j x };
foldr c n l = flst l n (\h t -> c h(foldr c n t));
foldr1 c l = maybe undefined id (flst l undefined (\h t -> foldr (\x m -> Just (case m of { Nothing -> x ; Just y -> c x y })) Nothing l));
foldl f a bs = foldr (\b g x -> g (f x b)) (\x -> x) bs a;
foldl1 f bs = flst bs undefined (\h t -> foldl f h t);
elem k xs = foldr (\x t -> ife (x == k) True t) False xs;
find f xs = foldr (\x t -> ife (f x) (Just x) t) Nothing xs;
(++) = flip (foldr (:));
concat = foldr (++) [];
wrap c = c:[];
map = flip (foldr . ((:) .)) [];
concatMap = (concat .) . map;
fmaybe m n j = case m of { Nothing -> n; Just x -> j x };
lookup s = foldr (\h t -> fpair h (\k v -> ife (s == k) (Just v) t)) Nothing;
-- Map.
data Map k a = Tip | Bin Int k a (Map k a) (Map k a);
size m = case m of { Tip -> 0 ; Bin sz _ _ _ _ -> sz };
node k x l r = Bin (succ $ size l + size r) k x l r;
singleton k x = Bin 1 k x Tip Tip;
singleL k x l r = case r of
{ Tip -> undefined
; Bin _ rk rkx rl rr -> node rk rkx (node k x l rl) rr
};
singleR k x l r = case l of
{ Tip -> undefined
; Bin _ lk lkx ll lr -> node lk lkx ll (node k x lr r)
};
doubleL k x l r = case r of
{ Tip -> undefined
; Bin _ rk rkx rl rr -> case rl of
{ Tip -> undefined
; Bin _ rlk rlkx rll rlr -> node rlk rlkx (node k x l rll) (node rk rkx rlr rr)
}
};
doubleR k x l r = case l of
{ Tip -> undefined
; Bin _ lk lkx ll lr -> case lr of
{ Tip -> undefined
; Bin _ lrk lrkx lrl lrr -> node lrk lrkx (node lk lkx ll lrl) (node k x lrr r)
}
};
balance k x l r = case size l + size r <= 1 of
{ True -> node
; False -> case 5 * size l + 3 <= 2 * size r of
{ True -> case r of
{ Tip -> node
; Bin sz _ _ rl rr -> case 3 * size rr <= 2 * size rl of
{ True -> doubleL
; False -> singleL
}
}
; False -> case 5 * size r + 3 <= 2 * size l of
{ True -> case l of
{ Tip -> node
; Bin sz _ _ ll lr -> case 3 * size ll <= 2 * size lr of
{ True -> doubleR
; False -> singleR
}
}
; False -> node
}
}
} k x l r;
insert kx x t = case t of
{ Tip -> singleton kx x
; Bin sz ky y l r -> case compare kx ky of
{ LT -> balance ky y (insert kx x l) r
; GT -> balance ky y l (insert kx x r)
; EQ -> Bin sz kx x l r
}
};
mlookup kx t = case t of
{ Tip -> Nothing
; Bin _ ky y l r -> case compare kx ky of
{ LT -> mlookup kx l
; GT -> mlookup kx r
; EQ -> Just y
}
};
fromList = let
{ ins t kx = case kx of { (,) k x -> insert k x t }
} in foldl ins Tip;
foldrWithKey f = let
{ go z t = case t of
{ Tip -> z
; Bin _ kx x l r -> go (f kx x (go z r)) l
}
} in go;
toAscList = foldrWithKey (\k x xs -> (k,x):xs) [];
-- Parsing.
data Type = TC String | TV String | TAp Type Type;
data Extra = Basic Int | Const Int | StrCon String | Proof Pred;
data Ast = E Extra | V String | A Ast Ast | L String Ast;
ro = E . Basic . ord;
pure x = \inp -> Just (x, inp);
sat' f = \h t -> ife (f h) (pure h t) Nothing;
sat f inp = flst inp Nothing (sat' f);
bind f m = case m of
{ Nothing -> Nothing
; Just x -> fpair x f
};
ap x y = \inp -> bind (\a t -> bind (\b u -> pure (a b) u) (y t)) (x inp);
(<*>) = ap;
fmap f x = ap (pure f) x;
(<$>) = fmap;
(>>=) x y = \inp -> bind (\a t -> y a t) (x inp);
(<|>) x y = \inp -> case x inp of
{ Nothing -> y inp
; Just x -> Just x
};
liftA2 f x y = ap (fmap f x) y;
(*>) = liftA2 \x y -> y;
(<*) = liftA2 \x y -> x;
many p = liftA2 (:) p (many p) <|> pure [];
some p = liftA2 (:) p (many p);
sepBy1 p sep = liftA2 (:) p (many (sep *> p));
sepBy p sep = sepBy1 p sep <|> pure [];
char c = sat \x -> x == c;
between x y p = x *> (p <* y);
com = char '-' *> between (char '-') (char '\n') (many (sat \c -> not (c == '\n')));
sp = many ((wrap <$> (sat (\c -> (c == ' ') || (c == '\n')))) <|> com);
spc f = f <* sp;
spch = spc . char;
wantWith pred f inp = bind (sat' pred) (f inp);
want f s inp = wantWith (s ==) f inp;
paren = between (spch '(') (spch ')');
small = sat \x -> ((x <= 'z') && ('a' <= x)) || (x == '_');
large = sat \x -> (x <= 'Z') && ('A' <= x);
digit = sat \x -> (x <= '9') && ('0' <= x);
varLex = liftA2 (:) small (many (small <|> large <|> digit <|> char '\''));
conId = spc (liftA2 (:) large (many (small <|> large <|> digit <|> char '\'')));
keyword s = spc (want varLex s);
varId = spc (wantWith (\s -> not $ s == "of" || s == "where") varLex);
opLex = some (sat (\c -> elem c ":!#$%&*+./<=>?@\\^|-~"));
op = spc opLex <|> between (spch '`') (spch '`') varId;
var = varId <|> paren (spc opLex);
listify = foldr (\h t -> A (A (V ":") h) t) (V "[]");
escChar = char '\\' *> ((sat (\c -> elem c "'\"\\")) <|> ((\c -> '\n') <$> char 'n'));
litOne delim = escChar <|> sat \c -> not (c == delim);
litInt = E . Const . foldl (\n d -> 10*n + ord d - ord '0') 0 <$> spc (some digit);
litStr = between (char '"') (spch '"') $ E . StrCon <$> many (litOne '"');
litChar = E . Const . ord <$> between (char '\'') (spch '\'') (litOne '\'');
lit = litStr <|> litChar <|> litInt;
sqLst r = between (spch '[') (spch ']') $ listify <$> sepBy r (spch ',');
alt r = (,) <$> (conId <|> (wrap <$> paren (spch ':' <|> spch ',')) <|> ((:) <$> spch '[' <*> (wrap <$> spch ']'))) <*> (flip (foldr L) <$> many varId <*> (want op "->" *> r));
braceSep f = between (spch '{') (spch '}') (sepBy f (spch ';'));
alts r = braceSep (alt r);
cas' x as = foldl A (V (concatMap (('|':) . fst) as)) (x:map snd as);
cas r = cas' <$> between (keyword "case") (keyword "of") r <*> alts r;
lamCase r = keyword "case" *> (L "of" . cas' (V "of") <$> alts r);
lam r = spch '\\' *> (lamCase r <|> liftA2 (flip (foldr L)) (some varId) (char '-' *> (spch '>' *> r)));
thenComma r = spch ',' *> (((\x y -> A (A (V ",") y) x) <$> r) <|> pure (A (V ",")));
parenExpr r = (&) <$> r <*> (((\v a -> A (V v) a) <$> op) <|> thenComma r <|> pure id);
rightSect r = ((\v a -> L "@" $ A (A (V v) $ V "@") a) <$> (op <|> (wrap <$> spch ','))) <*> r;
section r = paren (parenExpr r <|> rightSect r);
isFree v expr = case expr of
{ E _ -> False
; V s -> s == v
; A x y -> isFree v x || isFree v y
; L w t -> not (v == w) && isFree v t
};
maybeFix s x = ife (isFree s x) (A (ro 'Y') (L s x)) x;
def r = liftA2 (,) var (liftA2 (flip (foldr L)) (many varId) (spch '=' *> r));
addLets ls x = foldr (\p t -> fpair p (\name def -> A (L name t) $ maybeFix name def)) x ls;
letin r = addLets <$> between (keyword "let") (keyword "in") (braceSep (def r)) <*> r;
atom r = letin r <|> sqLst r <|> section r <|> cas r <|> lam r <|> (paren (spch ',') *> pure (V ",")) <|> fmap V (conId <|> var) <|> lit;
aexp r = fmap (foldl1 A) (some (atom r));
fix f = f (fix f);
data Assoc = NAssoc | LAssoc | RAssoc;
eqAssoc x y = case x of
{ NAssoc -> case y of { NAssoc -> True ; LAssoc -> False ; RAssoc -> False }
; LAssoc -> case y of { NAssoc -> False ; LAssoc -> True ; RAssoc -> False }
; RAssoc -> case y of { NAssoc -> False ; LAssoc -> False ; RAssoc -> True }
};
precOf s precTab = fmaybe (lookup s precTab) 9 fst;
assocOf s precTab = fmaybe (lookup s precTab) LAssoc snd;
opWithPrec precTab n = wantWith (\s -> n == precOf s precTab) op;
opFold precTab e xs = case xs of
{ [] -> e
; (:) x xt -> case find (\y -> not (eqAssoc (assocOf (fst x) precTab) (assocOf (fst y) precTab))) xt of
{ Nothing -> case assocOf (fst x) precTab of
{ NAssoc -> case xt of
{ [] -> fpair x (\op y -> A (A (V op) e) y)
; (:) y yt -> undefined
}
; LAssoc -> foldl (\a b -> fpair b (\op y -> A (A (V op) a) y)) e xs
; RAssoc -> (foldr (\a b -> fpair a (\op y -> \e -> A (A (V op) e) (b y))) id xs) e
}
; Just y -> undefined
}
};
expr precTab = fix \r n -> ife (n <= 9) (liftA2 (opFold precTab) (r (succ n)) (many (liftA2 (\a b -> (a,b)) (opWithPrec precTab n) (r (succ n))))) (aexp (r 0));
data Constr = Constr String [Type];
data Pred = Pred String Type;
data Qual = Qual [Pred] Type;
data Top = Adt Type [Constr] | Def (String, Ast) | Class String Type [(String, Type)] | Inst String Qual [(String, Ast)];
arr a b = TAp (TAp (TC "->") a) b;
bType r = foldl1 TAp <$> some r;
_type r = foldr1 arr <$> sepBy (bType r) (spc (want opLex "->"));
typeConst = (\s -> ife (s == "String") (TAp (TC "[]") (TC "Int")) (TC s)) <$> conId;
aType = paren ((&) <$> _type aType <*> ((spch ',' *> ((\a b -> TAp (TAp (TC ",") b) a) <$> _type aType)) <|> pure id)) <|>
typeConst <|> (TV <$> varId) <|>
(spch '[' *> (spch ']' *> pure (TC "[]") <|> TAp (TC "[]") <$> (_type aType <* spch ']')));
simpleType c vs = foldl TAp (TC c) (map TV vs);
adt = Adt <$> between (keyword "data") (spch '=') (simpleType <$> conId <*> many varId) <*> (sepBy (Constr <$> conId <*> many aType) (spch '|'));
prec = (\c -> ord c - ord '0') <$> spc digit;
fixityList a n os = map (\o -> (o, (n, a))) os;
fixityDecl kw a = between (keyword kw) (spch ';') (fixityList a <$> prec <*> sepBy op (spch ','));
fixity = fixityDecl "infix" NAssoc <|> fixityDecl "infixl" LAssoc <|> fixityDecl "infixr" RAssoc;
noQual = Qual [];
genDecl = (,) <$> var <*> (char ':' *> spch ':' *> _type aType);
classDecl = keyword "class" *> (Class <$> conId <*> (TV <$> varId) <*> (keyword "where" *> braceSep genDecl));
inst = _type aType;
instDecl r = keyword "instance" *>
((\ps cl ty defs -> Inst cl (Qual ps ty) defs) <$>
(((wrap .) . Pred <$> conId <*> (inst <* want op "=>")) <|> pure [])
<*> conId <*> inst <*> (keyword "where" *> braceSep (def r)));
tops precTab = sepBy
( adt
<|> Def <$> def (expr precTab 0)
<|> classDecl
<|> instDecl (expr precTab 0)
) (spch ';');
program' = sp *> (((":", (5, RAssoc)):) . concat <$> many fixity) >>= tops;
-- Primitives.
program = (
[ Adt (TAp (TC "[]") (TV "a")) [Constr "[]" [], Constr ":" [TV "a", TAp (TC "[]") (TV "a")]]
, Adt (TAp (TAp (TC ",") (TV "a")) (TV "b")) [Constr "," [TV "a", TV "b"]]] ++) <$> program';
prims = let
{ ii = arr (TC "Int") (TC "Int")
; iii = arr (TC "Int") ii
; bin s = A (A (ro 'B') (ro 'T')) (A (ro 'T') (ro s)) } in map (second (first noQual)) $
[ ("intEq", (arr (TC "Int") (arr (TC "Int") (TC "Bool")), bin '='))
, ("intLE", (arr (TC "Int") (arr (TC "Int") (TC "Bool")), bin 'L'))
, ("chr", (ii, ro 'I'))
, ("ord", (ii, ro 'I'))
, ("succ", (ii, A (ro 'T') (A (E $ Const $ 1) (ro '+'))))
, ("putChar", (arr (TC "Int") (TAp (TC "IO") (TV "a")), A (ro 'T') (A (ro 'F') (ro $ chr 1))))
, ("ioBind", (arr (TAp (TC "IO") (TV "a")) (arr (arr (TV "a") (TAp (TC "IO") (TV "b"))) (TAp (TC "IO") (TV "b"))), ro 'C'))
, ("ioPure", (arr (TV "a") (TAp (TC "IO") (TV "a")), ro 'V'))
] ++ map (\s -> (wrap s, (iii, bin s))) "+-*/%";
ifz n = ife (0 == n);
showInt' n = ifz n id ((showInt' (n/10)) . ((:) (chr (48+(n%10)))));
showInt n s = ifz n ('0':) (showInt' n) s;
-- Conversion to De Bruijn indices.
data LC = Ze | Su LC | Pass Int | La LC | App LC LC;
debruijn m n e = case e of
{ E x -> case x of
{ Basic b -> Pass b
; Const c -> App (Pass $ ord '#') (Pass c)
-- More principled perhaps:
-- ; StrCon s -> debruijn m n $ listify $ map (E . Const . ord) s
; StrCon s -> foldr (\h t -> App (App (Pass $ ord ':') (App (Pass $ ord '#') (Pass $ ord h))) t) (Pass $ ord 'K') s
; Proof _ -> undefined
}
; V v -> maybe (fmaybe (mlookup v m) undefined Pass) id $
foldr (\h found -> ife (h == v) (Just Ze) (maybe Nothing (Just . Su) found)) Nothing n
; A x y -> App (debruijn m n x) (debruijn m n y)
; L s t -> La (debruijn m (s:n) t)
};
-- Kiselyov bracket abstraction.
data IntTree = Lf Int | Nd IntTree IntTree;
data Sem = Defer | Closed IntTree | Need Sem | Weak Sem;
lf = Lf . ord;
ldef = \r y -> case y of
{ Defer -> Need (Closed (Nd (Nd (lf 'S') (lf 'I')) (lf 'I')))
; Closed d -> Need (Closed (Nd (lf 'T') d))
; Need e -> Need (r (Closed (Nd (lf 'S') (lf 'I'))) e)
; Weak e -> Need (r (Closed (lf 'T')) e)
};
lclo = \r d y -> case y of
{ Defer -> Need (Closed d)
; Closed dd -> Closed (Nd d dd)
; Need e -> Need (r (Closed (Nd (lf 'B') d)) e)
; Weak e -> Weak (r (Closed d) e)
};
lnee = \r e y -> case y of
{ Defer -> Need (r (r (Closed (lf 'S')) e) (Closed (lf 'I')))
; Closed d -> Need (r (Closed (Nd (lf 'R') d)) e)
; Need ee -> Need (r (r (Closed (lf 'S')) e) ee)
; Weak ee -> Need (r (r (Closed (lf 'C')) e) ee)
};
lwea = \r e y -> case y of
{ Defer -> Need e
; Closed d -> Weak (r e (Closed d))
; Need ee -> Need (r (r (Closed (lf 'B')) e) ee)
; Weak ee -> Weak (r e ee)
};
babsa x y = case x of
{ Defer -> ldef babsa y
; Closed d -> lclo babsa d y
; Need e -> lnee babsa e y
; Weak e -> lwea babsa e y
};
babs t = case t of
{ Ze -> Defer
; Su x -> Weak (babs x)
; Pass n -> Closed (Lf n)
; La t -> case babs t of
{ Defer -> Closed (lf 'I')
; Closed d -> Closed (Nd (lf 'K') d)
; Need e -> e
; Weak e -> babsa (Closed (lf 'K')) e
}
; App x y -> babsa (babs x) (babs y)
};
nolam m x = case babs $ debruijn m [] x of
{ Defer -> undefined
; Closed d -> d
; Need e -> undefined
; Weak e -> undefined
};
enc mem t = case t of
{ Lf n -> (n, mem)
; Nd x y -> fpair (enc mem x) \p mem' -> fpair (enc mem' y) \q mem'' ->
ife (p == ord 'I') (q, mem'') $
ife (q == ord 'I') (
ife (p == ord 'C') (ord 'T', mem) $
ife (p == ord 'B') (ord 'I', mem) $
fpair mem'' \hp bs -> (hp, (hp + 2, bs . (p:) . (q:)))
) $
fpair mem'' \hp bs -> (hp, (hp + 2, bs . (p:) . (q:)))
};
asm qas = foldl (\tabmem def -> fpair def \s qt -> fpair tabmem \tab mem ->
fpair (enc mem $ nolam tab $ snd qt) \p m' -> (insert s p tab, m'))
(Tip, (128, id)) qas;
-- Type checking.
apply sub t = case t of
{ TC v -> t
; TV v -> fmaybe (lookup v sub) t id
; TAp a b -> TAp (apply sub a) (apply sub b)
};
(@@) s1 s2 = map (second (apply s1)) s2 ++ s1;
occurs s t = case t of
{ TC v -> False
; TV v -> s == v
; TAp a b -> occurs s a || occurs s b
};
varBind s t = case t of
{ TC v -> Just [(s, t)]
; TV v -> ife (v == s) (Just []) (Just [(s, t)])
; TAp a b -> ife (occurs s t) Nothing (Just [(s, t)])
};
charIsInt s = ife (s == "Char") "Int" s;
mgu unify t u = case t of
{ TC a -> case u of
{ TC b -> ife (charIsInt a == charIsInt b) (Just []) Nothing
; TV b -> varBind b t
; TAp a b -> Nothing
}
; TV a -> varBind a u
; TAp a b -> case u of
{ TC b -> Nothing
; TV b -> varBind b t
; TAp c d -> unify b d (mgu unify a c)
}
};
maybeMap f = maybe Nothing (Just . f);
unify a b = maybe Nothing \s -> maybeMap (@@ s) (mgu unify (apply s a) (apply s b));
--instantiate' :: Type -> Int -> [(String, Type)] -> ((Type, Int), [(String, Type)])
instantiate' t n tab = case t of
{ TC s -> ((t, n), tab)
; TV s -> case lookup s tab of
{ Nothing -> let { va = TV (showInt n "") } in ((va, succ n), (s, va):tab)
; Just v -> ((v, n), tab)
}
; TAp x y ->
fpair (instantiate' x n tab) \tn1 tab1 ->
fpair tn1 \t1 n1 -> fpair (instantiate' y n1 tab1) \tn2 tab2 ->
fpair tn2 \t2 n2 -> ((TAp t1 t2, n2), tab2)
};
instantiatePred pred xyz = case pred of { Pred s t -> fpair xyz \xy tab -> fpair xy \out n -> first (first ((:out) . Pred s)) (instantiate' t n tab) };
--instantiate :: Qual -> Int -> (Qual, Int)
instantiate qt n = case qt of { Qual ps t ->
fpair (foldr instantiatePred (([], n), []) ps) \xy tab -> fpair xy \ps1 n1 ->
first (Qual ps1) (fst (instantiate' t n1 tab))
};
--type SymTab = [(String, (Qual, Ast))];
--type Subst = [(String, Type)];
--infer' :: SymTab -> Subst -> Ast -> (Maybe Subst, Int) -> ((Type, Ast), (Maybe Subst, Int))
infer' typed loc ast csn = fpair csn \cs n ->
let
{ va = TV (showInt n "")
; insta ty = fpair (instantiate ty n) \q n1 -> case q of { Qual preds ty -> ((ty, foldl A ast (map (E . Proof) preds)), (cs, n1)) }
}
in case ast of
{ E x -> case x of
{ Basic b -> ife (b == ord 'Y')
(insta $ noQual $ arr (arr (TV "a") (TV "a")) (TV "a"))
undefined
; Const _ -> ((TC "Int", ast), csn)
; StrCon _ -> ((TAp (TC "[]") (TC "Int"), ast), csn)
; Proof _ -> undefined
}
; V s -> fmaybe (lookup s loc)
(fmaybe (lookup s typed) undefined $ insta . fst)
((, csn) . (, ast))
; A x y ->
fpair (infer' typed loc x (cs, succ n)) \tax csn1 -> fpair tax \tx ax ->
fpair (infer' typed loc y csn1) \tay csn2 -> fpair tay \ty ay ->
((va, A ax ay), first (unify tx (arr ty va)) csn2)
; L s x -> first (\ta -> fpair ta \t a -> (arr va t, L s a)) (infer' typed ((s, va):loc) x (cs, succ n))
};
onType f pred = case pred of { Pred s t -> Pred s (f t) };
instance Eq Type where { (==) t u = case t of
{ TC s -> case u of
{ TC t -> t == s
; TV _ -> False
; TAp _ _ -> False
}
; TV s -> case u of
{ TC _ -> False
; TV t -> t == s
; TAp _ _ -> False
}
; TAp a b -> case u of
{ TC _ -> False
; TV _ -> False
; TAp c d -> a == c && b == d
}
}};
instance Eq Pred where { (==) p q =
case p of { Pred s a -> case q of { Pred t b -> s == t && a == b }}};
predApply sub p = onType (apply sub) p;
all f = foldr (&&) True . map f;
filter f = foldr (\x xs ->ife (f x) (x:xs) xs) [];
intersect xs ys = filter (\x -> fmaybe (find (x ==) ys) False (\_ -> True)) xs;
merge s1 s2 = ife (all (\v -> apply s1 (TV v) == apply s2 (TV v))
$ map fst s1 `intersect` map fst s2) (Just $ s1 ++ s2) Nothing;
match h t = case h of
{ TC a -> case t of
{ TC b -> ife (a == b) (Just []) Nothing
; TV b -> Nothing
; TAp a b -> Nothing
}
; TV a -> Just [(a, t)]
; TAp a b -> case t of
{ TC b -> Nothing
; TV b -> Nothing
; TAp c d -> case match a c of
{ Nothing -> Nothing
; Just ac -> case match b d of
{ Nothing -> Nothing
; Just bd -> merge ac bd
}
}
}
};
matchPred h p = case p of { Pred _ t -> match h t };
showType t = case t of
{ TC s -> s
; TV s -> s
; TAp a b -> concat ["(", showType a, " ", showType b, ")"]
};
showPred p = case p of { Pred s t -> s ++ (' ':showType t) ++ " => "};
findInst r qn p insts = case insts of
{ [] ->
fpair qn \q n -> let { v = '*':showInt n "" } in (((p, v):q, succ n), V v)
; (:) i is -> case i of { Qual ps h -> case matchPred h p of
{ Nothing -> findInst r qn p is
; Just u -> foldl (\qnt p -> fpair qnt \qn1 t -> second (A t)
(r (predApply u p) qn1)) (qn, V (case p of { Pred s _ -> showPred $ Pred s h})) ps
}}};
findProof is pred psn = fpair psn \ps n -> case lookup pred ps of
{ Nothing -> case pred of { Pred s t -> case lookup s is of
{ Nothing -> undefined -- No instances!
; Just insts -> findInst (findProof is) psn pred insts
}}
; Just s -> (psn, V s)
};
prove' ienv sub psn a = case a of
{ E x -> case x of
{ Basic _ -> (psn, a)
; Const _ -> (psn, a)
; StrCon _ -> (psn, a)
; Proof raw -> findProof ienv (predApply sub raw) psn
}
; V _ -> (psn, a)
; A x y -> let { p1 = prove' ienv sub psn x } in fpair p1 \psn1 x1 ->
second (A x1) (prove' ienv sub psn1 y)
; L s t -> second (L s) (prove' ienv sub psn t)
};
--prove :: [(String, [Qual])] -> (Type, Ast) -> Subst -> (Qual, Ast)
prove ienv ta sub = fpair ta \t a ->
fpair (prove' ienv sub ([], 0) a) \psn x -> fpair psn \ps _ ->
(Qual (map fst ps) (apply sub t), foldr L x (map snd ps));
data Either a b = Left a | Right b;
dictVars ps n = flst ps ([], n) \p pt -> first ((p, '*':showInt n ""):) (dictVars pt $ succ n);
-- qi = Qual of instance, e.g. Eq t => [t] -> [t] -> Bool
inferMethod ienv typed qi def = fpair def \s expr ->
fpair (infer' typed [] expr (Just [], 0)) \ta msn ->
case lookup s typed of
{ Nothing -> undefined -- No such method.
-- e.g. qac = Eq a => a -> a -> Bool, some AST (product of single method)
; Just qac -> fpair msn \ms n -> case ms of
{ Nothing -> undefined -- Type check fails.
; Just sub -> fpair (instantiate (fst qac) n) \q1 n1 -> case q1 of { Qual psc tc -> case psc of
{ [] -> undefined -- Unreachable.
; (:) headPred shouldBeNull -> case qi of { Qual psi ti ->
case headPred of { Pred _ headT -> case match headT ti of
{ Nothing -> undefined
-- e.g. Eq t => [t] -> [t] -> Bool
-- instantiate and match it against type of ta
; Just subc ->
fpair (instantiate (Qual psi $ apply subc tc) n1) \q2 n2 ->
case q2 of { Qual ps2 t2 -> fpair ta \tx ax ->
case match (apply sub tx) t2 of
{ Nothing -> undefined -- Class/instance type conflict.
; Just subx -> snd $ prove' ienv (subx @@ sub) (dictVars ps2 0) ax
}}}}}}}}};
inferInst ienv typed inst = fpair inst \cl qds -> fpair qds \q ds ->
case q of { Qual ps t -> let { s = showPred $ Pred cl t } in
(s, (,) (noQual $ TC "DICT") $ maybeFix s $ foldr L (L "@" $ foldl A (V "@") (map (inferMethod ienv typed q) ds)) (map snd $ fst $ dictVars ps 0))
};
reverse = foldl (flip (:)) [];
inferDefs ienv defs typed = flst defs (Right $ reverse typed) \edef rest -> case edef of
{ Left def -> fpair def \s expr -> fpair (infer' typed [] (maybeFix s expr) (Just [], 0)) \ta msn ->
fpair msn \ms _ -> case maybeMap (prove ienv ta) ms of
{ Nothing -> Left ("bad type: " ++ s)
; Just qa -> inferDefs ienv rest ((s, qa):typed)
}
; Right inst -> inferDefs ienv rest (inferInst ienv typed inst:typed)
};
conOf con = case con of { Constr s _ -> s };
mkCase t cs = (concatMap (('|':) . conOf) cs,
( noQual $ arr t $ foldr arr (TV "case") $ map (\c -> case c of { Constr _ ts -> foldr arr (TV "case") ts}) cs
, ro 'I'));
mkStrs = snd . foldl (\p u -> fpair p (\s l -> ('@':s, s : l))) ("@", []);
length = foldr (\_ n -> succ n) 0;
scottEncode vs s ts = foldr L (foldl (\a b -> A a (V b)) (V s) ts) (ts ++ vs);
scottConstr t cs c = case c of { Constr s ts -> (s,
( noQual $ foldr arr t ts
, scottEncode (map conOf cs) s $ mkStrs ts)) };
mkAdtDefs t cs = mkCase t cs : map (scottConstr t cs) cs;
-- * instance environment
-- * definitions, including those of instances
-- * Typed ASTs, ready for compilation, including ADTs and methods,
-- e.g. (==), (Eq a => a -> a -> Bool, select-==)
data Neat = Neat [(String, [Qual])] [Either (String, Ast) (String, (Qual, [(String, Ast)]))] [(String, (Qual, Ast))];
fneat neat f = case neat of { Neat a b c -> f a b c };
select f xs acc = flst xs (Nothing, acc) \x xt -> ife (f x) (Just x, xt ++ acc) (select f xt (x:acc));
addInstance s q is = fpair (select (\kv -> s == fst kv) is []) \m xs -> case m of
{ Nothing -> (s, [q]):xs
; Just sqs -> second (q:) sqs:xs
};
mkSel ms s = L "*" $ A (V "*") $ foldr L (V $ '*':s) $ map (('*':) . fst) ms;
untangle = foldr (\top acc -> fneat acc \ienv fs typed -> case top of
{ Adt t cs -> Neat ienv fs (mkAdtDefs t cs ++ typed)
; Def f -> Neat ienv (Left f : fs) typed
; Class classId v ms -> Neat ienv fs (
map (\st -> fpair st \s t -> (s, (Qual [Pred classId v] t, mkSel ms s))) ms
++ typed)
; Inst cl q ds -> Neat (addInstance cl q ienv) (Right (cl, (q, ds)):fs) typed
}) (Neat [] [] prims);
infer prog = fneat (untangle prog) inferDefs;
showQual q = case q of { Qual ps t -> concatMap showPred ps ++ showType t };
dumpTypes s = fmaybe (program s) "parse error" \progRest ->
fpair progRest \prog rest -> case infer prog of
{ Left err -> err
; Right typed -> concatMap (\p -> fpair p \s qa -> s ++ " :: " ++ showQual (fst qa) ++ "\n") typed
};
prepAsm entry tabmem = fpair tabmem \tab mem ->
maybe undefined id (mlookup entry tab) : snd mem [];
last' x xt = flst xt x \y yt -> last' y yt;
last xs = flst xs undefined last';
compile s = fmaybe (program s) "parse error" \progRest ->
fpair progRest \prog rest -> case infer prog of
{ Left err -> err
; Right qas -> foldr (\n s -> showInt n $ ',':s) rest $ prepAsm (fst $ last qas) $ asm qas
}