The beauty of functional logic programming where unification is natively supported. I’m curious how this would scale up to HM.
data Ty = Iota | Arr Ty Ty data Tm = Var String | App Tm Tm | Lam String Tm infer ctx (Var x) = case lookup x ctx of Just t -> t Nothing -> error (x ++ " undefined") infer ctx (App e1 e2) | infer ctx e2 `Arr` t =:= infer ctx e1 = t where t free infer ctx (Lam x e) = t `Arr` infer ((x,t):ctx) e where t free
This actually runs in PAKCS well as below. There are some strange warnings from the prolog side, which I have no idea what they are about. And, I don’t really handle errors so messages when unification fails are not good of course.
______ __ _ _ ______ _______ | __ | / \ | | / / | ____| | _____| Portland Aachen Kiel | | | | / /\ \ | |_/ / | | | |_____ Curry System | |__| | / /__\ \ | _ | | | |_____ | | ____| / ______ \ | | \ \ | |____ _____| | Version 1.11.4 (4) |_| /_/ \_\ |_| \_\ |______| |_______| Curry2Prolog(swi 6.6) Compiler Environment (Version of 2014-11-22) (RWTH Aachen, CAU Kiel, Portland State University) Type ":h" for help (contact: email@example.com) Prelude> :l a [1 of 2] Skipping Prelude ( /home/kyagrd/cscs/pakcs/lib/Prelude.curry, /home/kyagrd/csc s/pakcs/lib/.curry/Prelude.fcy ) [2 of 2] Compiling a ( a.curry, .curry/a.fcy ) > :define x=Var "x" > :define y=Var "y" > :define z=Var "z" > infer  (Lam "x" x) Arr _a _a > infer  (Lam "x" (Lam "y" (Lam "z" (App (App x z) (App y z))))) Warning: /tmp/pl_pakcs_file_18510_8/.curry/pakcs/PAKCS_Main_Exp.pl:23: Redefined static procedure PAKCS_Main_Exp.pakcsMainGoal/3 Previously defined at /tmp/pl_pakcs_file_18510_7/.curry/pakcs/PAKCS_Main_Exp.pl:23 Warning: /tmp/pl_pakcs_file_18510_8/.curry/pakcs/PAKCS_Main_Exp.pl:24: Redefined static procedure blocked_PAKCS_Main_Exp.pakcsMainGoal/3 Previously defined at /tmp/pl_pakcs_file_18510_7/.curry/pakcs/PAKCS_Main_Exp.pl:24 Arr (Arr _a (Arr _b _c)) (Arr (Arr _a _b) (Arr _a _c)) > infer  (Lam "x" (App x x )) Warning: /tmp/pl_pakcs_file_18510_10/.curry/pakcs/PAKCS_Main_Exp.pl:23: Redefined static procedure PAKCS_Main_Exp.pakcsMainGoal/3 Previously defined at /tmp/pl_pakcs_file_18510_8/.curry/pakcs/PAKCS_Main_Exp.pl:23 Warning: /tmp/pl_pakcs_file_18510_10/.curry/pakcs/PAKCS_Main_Exp.pl:24: Redefined static procedure blocked_PAKCS_Main_Exp.pakcsMainGoal/3 Previously defined at /tmp/pl_pakcs_file_18510_8/.curry/pakcs/PAKCS_Main_Exp.pl:24 *** No value found!
Src also availiable at http://www-ps.informatik.uni-kiel.de/smap/smap.cgi?browser/31