Next Step: Kind and Type Checking

Looks like the module system is finished in that it passes a minimal unit test. I.e., given the next minimal non-sensical unit test:

import "util.hi"

namespace f.g (
    interface Some = #t where (
        def x : t-> v ->unit
    )

    instance Some int = (
        def x : unit = nop
    )
)

namespace i.j (
    def h: unit = nop
    def test: unit = h.f.g.x
)

namespace k (
    using f.g
    using i.j

    def test1: unit = h.x
)

type list = \a => [ nil | cons a (list a) ]

def ++: list a -> list a -> list a =
    [ nil, yy       -> yy
    | cons x xx, yy -> cons x (xx ++ yy) ]

That gets elaborated to

import "util.hi"
namespace f.g (
    interface f.g.SomeTC = (!vTV => #tTV where ( 
            method xC {SomeTC} : (tTV -> (vTV -> unitTC)) = (XXX)
        ))
    instance f.g.SomeTC f.g.intTC = (
            binding xC {intTC} : unitTC = nopC
        )
    select f.g.xC {f.g.SomeTC} : (!vTV => (!tTV => (::SomeTC tTC => (tTV -> (tTV -> (vTV -> unitTC)))))) = (XXX)
)
namespace i.j (
    def i.j.hC: unitTC = nopC
    def i.j.testC: unitTC = (i.j.hC@f.g.xC)
)
namespace k (
    using f.g
    using i.j
    def k.test1C: unitTC = (i.j.hC@f.g.xC)
)
type listTC = (\aTV => [ nilC{listTC} | consC{listTC} aTV (listTC aTV)])
def ++C: 
    (!aTV => ((listTC aTV) -> ((listTC aTV) -> (listTC aTV)))) = 
    [ nilC, yyV -> yyV | consC{list} xV xxV, yyV -> ((consC xV) ((++C xxV) yyV))]
record nilC{listTC}: (!aTV => (listTC aTV)) = nilC{listTC}
record consC{listTC}: 
    (!aTV => (aTV -> ((listTC aTV) -> (listTC aTV)))) = 
    \v#0V, v#1V -> consC{listTC} v#0V v#1V 

So, that's good enough for now.

The next step is deciding whether I am going to do semantical analysis or compile to LLVM code such that the interpreter will run. I decided to go for semantical analysis first.

The first step in semantical analysis is kindification, checking type denotations have the correct kinds. There are some minor design decisions in whether I'll attribute type definitions and type variables with kinds, or only semantically check code.

I also need to think over the scheme of how the kind, and later type, checker will work. What I do in the bootstrap compiler is gather up constraints in a bottom up fashion and dispatch the constraints to a general prover. I like that implementation but I am somewhat concerned about performance.

It's either: a) bottom up solve all constraints in situ, or b) bottom up gather constraints and dispatch to a prover and I don't know what to choose yet.