Hi Relegated

I concede. The minor typing systems I could come up with didn't handle all corner cases well. Instead of thinking about it more, I decided to start on a new untyped language.

Algorithm W

I like the prover in my bootstrap but, yeah, there's algorithm W too. So, I decided to go for that. Gone are the bisimulation proofs of type equivalences but I simply don't know what I am dropping there and can't care to figure it out. At least with W I know it has been proven correct, terminates, and gives reasonable performance on small terms.

Which also implies that I'll need to figure out how to do constraint checking with W. But, in some sense, W already checks constraints by providing a proof, a most general unifier, for types.

So. How hard can it be? Right...

Log 062115

Made a few small changes to the AST. Implementing a number of routines ahead of time until I figure out what to do with the type checker.

The type checker, as implemented in the bootstrap, is okay-ish. Not too shabby. The major difference between it and other functional type checker is that it records substitutions as type equivalences. I probably could speed it up already by factoring out different propositions. Moreover, I decided against using the gathered type equivalences to attribute the tree; I could do without recording substitutions.

Still, there's this thing about being able to typecheck cyclic types. Suppose, you have a type definition which unravels to the following:

              t
             / \
               /\
                 t
                / \
                  /\
                 .. ..

The type checker I now have "records" substitutions. It should therefore be able to prove type equivalences like the above by stating an equivalence, unfolding the type once, and using the postulated type. (Conceptually, the second "t" in the picture above becomes a cycle pointing to the first "t'.)

But that doesn't seem to be a problem in practice. To prove equivalences ML compilers simply unravel types a few times and use the definition to "close the cycle".

Ah well. First kindification I guess.

A Small Derivation

I completely forgot what my prover does; I rushed it anyway. So, I worked out a rough example by hand below to get some grasp on it. In a bottom up fashion it collects a mess of constraints, say it gathered

int:*∧ (::Ord int) ⊢t0:k0->t1:k1 = t2:k2 ∧ t2:k2 = int:ka->int:kb ∧ (::Ord t1)

It then proves that (roughly) likes this

int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4:* ∧ int:*= t3:k3 ∧ int:* = t4:k4 ∧ 

k0 = ka =* ∧ t0: = int:*∧ k1 = kb=* ∧ t1:* = int:* 

⊢

-----------------------------------------------------------

int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4:* ∧ int:*= t3:k3 ∧ int:* = t4:k4 ∧

 k0 = ka =* ∧ t0:* = int:*∧ k1= kb = * ∧ t1:* = int:* 

⊢ (::Ord int)

----------------------------------------------------------

int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4:* ∧ int:*= t3:k3 ∧ t1:k1 = t4:k4 

∧ k0 = ka =* ∧ t0:* = int:* 

⊢ t1:k1:* = int:kb ∧ (::Ord t1)

-----------------------------------------------------------

int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4:* ∧ t0:k0= t3:k3 ∧ t1:k1 = t4:k4 

⊢ t0:k0 = int:ka ∧ t1:k1 = int:kb ∧ (::Ord t1)

----------------------------------------------------------

int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4:* ∧ t0:k0= t3:k3 ∧ t1:k1 = t4:k4 

⊢ t0:k0->t1:k1 = int:ka->int:kb ∧ (::Ord t1)

---------------------------------------------------------

int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4 ∧ t0:k0= t3:k3 

⊢ t1:k1 = t4:k4 ∧ t0:k0->t4:k4 = int:ka->int:kb ∧ (::Ord t1)

-----------------------------------------------------

int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4 

⊢ t0:k0= t3:k3 ∧ t1:k1 = t4:k4 ∧ t3:k3->t4:k4 = int:ka->int:kb ∧ (::Ord t1)

----------------------------------------------------

int:*∧ (::Ord int) ⊢ t0:k0->t1:k1 = t2:k2 ∧ t2:k2 = int:ka->int:kb ∧ (::Ord t1)

So, okay. Guess that works. I made a reasonable estimate of how constraints should be solved, dump the mess in the prover, from the antecedent I read off how to attribute the tree with the solved constraints.

It doesn't seem to handle intermediaries well, though. Guess I need to check it with the algorithm. (Hmm. Intermediaries should remain on the left-hand side of the equation?)

Log 061815 - B

Right. I started implementing a general prover, then after the first few lines of code, decided against it. Thing is, I have a prover which works on terms like this

a₀ ∧ ... ∧ a_n ⊢c₀ ∧ ... ∧ c_m

It discharges each consequent given what it knows by inspecting the antecedents. Antecedents and consequents may be anything; e.g., kind equalities, type equalities, instantiation requests, etc. While proving a goal new consequents, sometimes an antecedent, may be introduced (trivially).

Thing is, I don't trust the time complexity of the algorithm. Checking for a consequent whether an antecedent exists is linear (times the term size of the antecedent), substitution is linear (times the term size), almost every step the prover takes is two of these linear, possibly quadratic, operations. As far as I know, proving in this general manner might be cubic.

So, I am working in the unknown here. Looks to me I want to keep the number of antecedents as far down as possible to keep the number of lookups and substitutions down, might also be that it is cubic but pragmatically that doesn't matter since you only operate on small numbers of small terms, lastly, since I sometimes am doing a 'bisimulation' proof, I might actually need to do it this way.

Stuck.

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.

Log 061815 - A

After I rewrote passing the environment through copying, that continued bugging me since copying is expensive. It also dawned to me where I made the mistake; I copied a local reference, modified that, and never passed it back before.

I rewrote the compiler such that the environment is passed as a pointer. It makes more sense and a lot of passes will use the environment, I didn't like the idea of spurious copying.

I also noticed again how computationally expensive the identification phase is, but I am not going to change that. It's just one pass and can hopefully easily be rewritten at a later stage.