Algorithm W for Hindley-Milner type inference

w.hoon

=>
|%
+$  exp
  $~  [%lit %int 0]
  $%  [%var =var]
      [%lit =lit]
      [%app fun=exp arg=exp]
      [%abs =var bod=exp]
      [%let =var val=exp bod=exp]
  ==
+$  lit
  $%  [%int val=@]
      [%wut val=?]
  ==
+$  typ
  $~  [%wut ~]
  $%  [%var =var]
      [%int ~]
      [%wut ~]
      [%fun fun=typ arg=typ]
  ==
+$  scheme  [vars=(list var) =typ]
+$  sub  (map var typ)
+$  env  (map var scheme)
+$  var  tape
--
=>
|%
++  ftv-typ
  |=  =typ
  ^-  (set var)
  ::
  ?-  -.typ
    %var  (~(put in *(set var)) typ)
    %int  ~
    %wut  ~
    %fun  (~(uni in $(typ fun.typ)) $(typ arg.typ))
  ==
::
++  apply-typ
  |=  [=sub =typ]
  ^+  typ
  ::
  ?+    -.typ  typ
    %var  (~(gut by sub) var.typ typ)
    %fun  [%fun $(typ fun.typ) $(typ arg.typ)]
  ==
::
++  ftv-scheme
  |=  =scheme
  ^-  (set var)
  ::
  (~(dif in (ftv-typ typ.scheme)) (sy vars.scheme))
::
++  apply-scheme
  |=  [=sub =scheme]
  ^+  scheme
  ::
  :-  vars.scheme
  %+  apply-typ  sub
  |-  ^+  typ.scheme
  ?~  vars.scheme  typ.scheme
  =.  sub  (~(del by sub) i.vars.scheme)
  $(vars.scheme t.vars.scheme)
::
++  ftv-env
  |=  =env
  ^-  (set var)
  ::
  %+  roll  ~(val by env)
  |=  [=scheme acc=(set var)]
  ^+  acc
  ::
  (~(uni in acc) (ftv-scheme scheme))
::
++  apply-env
  |=  [=sub =env]
  ^+  env
  ::
  %-  ~(gas by *(map var scheme))
  %+  turn  ~(tap by env)
  |=  [=var =scheme]
  ^+  +<
  [var (apply-scheme sub scheme)]
::
++  generalize
  |=  [=env =typ]
  ^-  scheme
  ::
  :_  typ
  %~  tap  in
  (~(dif in (ftv-typ typ)) (ftv-env env))
::
++  ti
  =|  ti-max=@
  =|  ti-sub=sub
  ::
  |%
  ++  ti-core  .
  ++  new-tv
    |=  prefix=var
    ^-  [typ _ti-core]
    ::
    :_  ti-core(ti-max +(ti-max))
    [%var (weld prefix (scow %ud ti-max))]
  ::
  ++  instantiate
    |=  =scheme
    ^-  [typ _ti-core]
    ::
    =^  typs  ti-core
      =|  typs=(list typ)
      |-  ^+  [typs ti-core]
      ?~  vars.scheme  [typs ti-core]
      =^  typ  ti-core  (new-tv "a")
      =.  typs  [typ typs]
      $(vars.scheme t.vars.scheme)
    ::
    =/  =sub
      %-  ~(gas by *(map var typ))
      |-  ^-  (list [var typ])
      ?~  typs  ~
      ?~  vars.scheme  ~
      :-  [i.vars.scheme i.typs]
      $(typs t.typs, vars.scheme t.vars.scheme)
    ::
    [(apply-typ sub typ.scheme) ti-core]
  ::
  ++  unify
    |=  [a=typ b=typ]
    ^-  [sub _ti-core]
    ::
    ?+  [-.a -.b]  !!
      [%int %int]  [~ ti-core]
      [%wut %wut]  [~ ti-core]
      [%var *]     ?>  ?=(%var -.a)  [(bind-var var.a b) ti-core]
      [* %var]     ?>  ?=(%var -.b)  [(bind-var var.b a) ti-core]
      [%fun %fun]
        ?>  ?=(%fun -.a)
        ?>  ?=(%fun -.b)
        =^  sub1  ti-core  $(a fun.a, b fun.b)
        =/  a-subbed  (apply-typ sub1 arg.a)
        =/  b-subbed  (apply-typ sub1 arg.b)
        =^  sub2  ti-core  $(a a-subbed, b b-subbed)
        [(~(uni by sub1) sub2) ti-core]
    ==
  ::
  ++  bind-var
    |=  [=var =typ]
    ^-  sub
    ::
    ?:  =(typ [%var var])
      ~
    ?<  (~(has in (ftv-typ typ)) var)
    (~(put by *sub) var typ)
  ::
  ++  infer-type
    |=  [=env =exp]
    ^-  [[=sub =typ] _ti-core]
    ::
    ?-    -.exp
        %var
      =/  =scheme  (~(got by env) var.exp)
      =^  typ  ti-core  (instantiate scheme)
      [[~ typ] ti-core]
    ::
        %lit
      =/  typ
        ?-  -.lit.exp
          %int  [%int ~]
          %wut  [%wut ~]
        ==
      [[~ typ] ti-core]
    ::
        %abs
      =^  new  ti-core  (new-tv "a")
      =.  env  (~(put by env) var.exp `scheme`[~ new])
      =^  res  ti-core  $(exp bod.exp)
      =.  typ.res  [%fun (apply-typ sub.res new) typ.res]
      [res ti-core]
    ::
        %app
      =^  new  ti-core  (new-tv "a")
      =^  fun  ti-core  $(exp fun.exp)  
      =^  arg  ti-core  $(exp arg.exp, env (apply-env sub.fun env))
      =^  res  ti-core  (unify (apply-typ sub.arg typ.fun) [%fun typ.arg new])
      =/  =sub  (~(uni in sub.fun) (~(uni in sub.arg) res))
      =/  =typ  (apply-typ res new)
      [[sub typ] ti-core]
    ::
        %let
      =^  val  ti-core  $(exp val.exp)
      =/  =scheme  (generalize (apply-env sub.val env) typ.val)
      =.  env  (~(put by env) var.exp scheme)
      =.  env  (apply-env sub.val env)
      =^  res  ti-core  $(exp bod.exp)
      =/  =sub  (~(uni in sub.val) sub.res)
      [[sub typ.res] ti-core]
    ==
  --
--
::  naked generator wrapper
::
|=  =exp
^-  typ
typ:(infer-type:ti *env exp)