ITT WIP

itt_wip.hvml

data List {
  #Nil
  #Cons{head tail}
}

data Pair {
  #Pair{fst snd}
}

data Term {
  #Var{nam}
  #Lam{nam bod}
  #App{fun arg}
  #Typ{nam bod}
  #Ann{val typ}
  #Sub{val}
}

data State {
  #State{ eqs val }
}

// Utils
// -----

@cat(xs ys) = ~xs !ys {
  #Nil: ys
  #Cons{h t}: #Cons{h @cat(t ys)}
}

@join(xs) = ~xs {
  #Nil: #Nil
  #Cons{h t}: @cat(h @join(t))
}

@same(a b) = ~a !b {
  #Nil: ~b {
    #Nil: 1
    #Cons{bh bt}: 0
  }
  #Cons{ah at}: ~b {
    #Nil: 0
    #Cons{bh bt}: (& (== ah bh) @same(at bt))
  }
}

// ITT Monad
// ---------

@bind(a f) = λeqs ~(a eqs) {
  #State{eqs val}: (f val eqs)
}

@pure(val) = λeqs #State{eqs val}

@push(eq) = λeqs #State{#Cons{eq eqs} 0}

// Stringification
// ---------------

@show(term) = ~term {
  #Var{nam}: nam
  #Lam{nam bod}: !&0{n0 n1}=nam @join(["λ" n0 " " @show((bod #Var{n1}))])
  #App{fun arg}: @join(["(" @show(fun) " " @show(arg) ")"])
  #Typ{nam bod}: !&0{n0 n1}=nam @join(["θ" n0 " " @show((bod #Var{n1}))])
  #Ann{val typ}: @join(["{" @show(val) ":" @show(typ) "}"])
  #Sub{val}: @join(["." @show(val)])
}

@show_eqs(eqs) = ~eqs {
  #Nil: "⊤"
  #Cons{h t}: ~h {
    #Pair{a b}: @join([@show(a) " = " @show(b) " & " @show_eqs(t)])
  }
}

// Evaluation
// ----------

@wnf(term) = ~term {
  #Var{nam}: #Var{nam}
  #Lam{nam bod}: #Lam{nam bod}
  #App{fun arg}: @app(@wnf(fun) arg)
  #Typ{nam bod}: #Typ{nam bod}
  #Ann{val typ}: @ann(val @wnf(typ))
  #Sub{val}: #Sub{val}
}

@app(f x) = ~f !x {
  #Var{nam}: #App{#Var{nam} x}
  #Lam{nam bod}: @wnf((bod @wnf(x)))
  #App{fun arg}: #App{#App{fun arg} x}
  #Typ{nam bod}: #Typ{nam λy #App{(bod #Lam{"_" λ$k(y)}) #Ann{$k x}}}
  #Ann{val typ}: #App{#Ann{val typ} x}
  #Sub{val}: #App{#Sub{val} x}
}

@ann(v t) = ~t !v {
  #Var{nam}: #Ann{v #Var{nam}}
  #Lam{nam bod}: #Lam{nam λy #Ann{#App{v $k} (bod #Typ{"_" λ$k(y)})}}
  #App{fun arg}: #Ann{v #App{fun arg}}
  #Typ{nam bod}: @wnf((bod @wnf(v)))
  #Ann{val typ}: #Ann{v #Ann{val typ}}
  #Sub{val}: #Ann{v #Sub{val}}
}

// Normalization
// -------------

@nf(term) = ~ @wnf(term) {
  #Var{nam}: #Var{nam}
  #Lam{nam bod}: #Lam{nam λx @nf((bod #Sub{x}))}
  #App{fun arg}: #App{@nf(fun) @nf(arg)}
  #Typ{nam bod}: #Typ{nam λx @nf((bod #Sub{x}))}
  #Ann{val typ}: #Ann{@nf(val) @nf(typ)}
  #Sub{val}: val
}

// Equality
// --------

// FIXME: generate fresh ids for var comparisons
@eq(a b) = ~ @wnf(a) !b {
  #Var{a_nam}: ~ @wnf(b) {
    #Var{b_nam}: @same(a_nam b_nam)
    #Lam{b_nam b_bod}: 0
    #App{b_fun b_arg}: 0
    #Typ{b_nam b_bod}: 0
    #Ann{b_val b_typ}: 0
    #Sub{b_val}: 0
  }
  #Lam{a_nam a_bod}: ~ @wnf(b) {
    #Var{b_nam}: 0
    #Lam{b_nam b_bod}: @eq((a_bod #Var{a_nam}) (b_bod #Var{b_nam}))
    #App{b_fun b_arg}: 0
    #Typ{b_nam b_bod}: 0
    #Ann{b_val b_typ}: 0
    #Sub{b_val}: 0
  }
  #App{a_fun a_arg}: ~ @wnf(b) {
    #Var{b_nam}: 0
    #Lam{b_nam b_bod}: 0
    #App{b_fun b_arg}: (& @eq(a_fun b_fun) @eq(a_arg b_arg))
    #Typ{b_nam b_bod}: 0
    #Ann{b_val b_typ}: 0
    #Sub{b_val}: 0
  }
  #Typ{a_nam a_bod}: ~ @wnf(b) {
    #Var{b_nam}: 0
    #Lam{b_nam b_bod}: 0
    #App{b_fun b_arg}: 0
    #Typ{b_nam b_bod}: @eq((a_bod #Var{a_nam}) (b_bod #Var{b_nam}))
    #Ann{b_val b_typ}: 0
    #Sub{b_val}: 0
  }
  #Ann{a_val a_typ}: ~ @wnf(b) {
    #Var{b_nam}: 0
    #Lam{b_nam b_bod}: 0
    #App{b_fun b_arg}: 0
    #Typ{b_nam b_bod}: 0
    #Ann{b_val b_typ}: (& @eq(a_val b_val) @eq(a_typ b_typ))
    #Sub{b_val}: 0
  }
  #Sub{a_val}: ~ @wnf(b) {
    #Var{b_nam}: 0
    #Lam{b_nam b_bod}: 0
    #App{b_fun b_arg}: 0
    #Typ{b_nam b_bod}: 0
    #Ann{b_val b_typ}: 0
    #Sub{b_val}: @eq(a_val b_val)
  }
}

// Checking
// --------

@check(tm) = ~ tm {
  #Var{nam}: *
  #Lam{nam bod}: *
  #App{fun arg}:
    @bind(@check(fun) λft
    @pure(@wnf(#App{ft arg})))
  #Typ{nam bod}: *
  #Ann{val typ}:
    !&2{t0 t1}=typ
    @bind(@valid(#Ann{val t0}) λ_
    @pure(@wnf(#Ann{#Var{"_"} t1})))
  #Sub{val}: *
}

@valid(tm) = ~ @wnf(tm) {
  #Var{nam}: @pure(0)
  #Lam{nam bod}: @valid((bod #Var{nam}))
  #App{fun arg}: @bind(@valid(fun) λ_ @valid(arg))
  #Typ{nam bod}: *
  #Ann{val typ}: ~ @wnf(val) {
    #Var{_}: *
    #Lam{_ _}: *
    #App{_ _}: *
    #Typ{_ _}: *
    #Ann{v t}: @bind(@push(#Pair{typ t}) λ_ @valid(v))
    #Sub{_}: *
  }
  #Sub{val}: *
}

// -----

// @idf = λx (x)
@idf = #Lam{"x" λx(x)}

// @c2 = λf λx (f (f x))
@c2 = #Lam{"f" λf #Lam{"x" λx !&1{f0 f1}=f #App{f0 #App{f1 x}}}}

// @k2 = λg λy (g (g y))
@k2 = #Lam{"g" λf #Lam{"y" λx !&2{f0 f1}=f #App{f0 #App{f1 x}}}}

// `∀F(X:A)->B` ::= @Fun(F X A B) = θf λx {(f {x:A}): B}
@Fun(F X A B) = #Typ{F λf #Lam{X λx #Ann{#App{f #Ann{x A}} B}}}

// @t0 = (@c2 @k2)
@t0 = #App{@c2 @k2}

// @t1 = {λx(x) : T -> T}
@t1 =
  ! val = @idf
  ! typ = @Fun("f" "x" #Var{"T"} #Var{"T"})
  #Ann{@idf typ}

// @t2 = {λaλbλc(a) : A -> B -> C -> A}
@t2 =
  ! val = #Lam{"a" λa #Lam{"b" λb #Lam{"c" λc a}}}
  ! typ = 
    @Fun("f" "x" #Var{"A"}
    @Fun("g" "y" #Var{"B"}
    @Fun("h" "z" #Var{"C"}
    #Var{"A"})))
  #Ann{val typ}

// @t3 = {λfλx(f x) : (A -> A) -> A -> A}
@t3 =
  ! val = #Lam{"f" λf #Lam{"x" λx #App{f x}}}
  ! typ =
    @Fun("f" "x" @Fun("ff" "fx" #Var{"A"} #Var{"A"})
    @Fun("g" "y" #Var{"A"}
    #Var{"A"}))
  #Ann{val typ}

// @t4 = {λfλgλx(f (g x)) : (B -> C) -> (A -> B) -> A -> C
@t4 =
  ! val = #Lam{"f" λf #Lam{"g" λg #Lam{"x" λx #App{f #App{g x}}}}}
  ! typ =
    @Fun("f" "x" @Fun("ff" "fx" #Var{"B"} #Var{"C"})
    @Fun("g" "y" @Fun("gg" "gy" #Var{"A"} #Var{"B"})
    @Fun("h" "z" #Var{"A"}
    #Var{"C"})))
  #Ann{val typ}

@main = ~ (@check(@t4) #Nil) {
  #State{eqs typ}: @show_eqs(eqs)
}