Day 2: Rank-2 polymorphism

I almost forgot to write-up today's work! ^^"

I added forall types to Growl's type system. This is because expressing some higher-order combinators requires rank-2 polymorphism, which means that types where quotations themselves have forall quantification must be valid and expressible.

I use a De Brujin-style representation, where a type can be wrapped in many Forall nodes, and QVar nodes count up from zero being the innermost forall node upwards, so the type for a stack shuffling word like over is expressed as ∀(∀(∀('λ2 'λ1 'λ0 → 'λ1 'λ2 'λ1 'λ0)))

I also have been reading about how Cat uses a concept called "self types" to express limited equi-recursion in types, which allows for types like the one of dup call to be expressible by marking the quotation as being able to accept itself without making it a proper recursive type.

Tomorrow I will likely implement self types, and move the type inference engine to a bi-directional inference system to support for type annotations. This will be needed for more complex expressions that might need some help from the user for the type inference to be able to do its job...

On the personal note, I got prescribed Ritalin. Let's see how that goes.

Listening to: Peace Forever Eternal – Reveille (In Loving Memory)