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: pakcs@curry-language.org)
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