[TYPES/announce] Request for Help for getting a Type Inferencer Right

[M.C.A. (Marco) Devillers]

Dear all,

I guess this is a somewhat unexpected request for a type theory list,
but thought I would like to post it anyway.

As an experiment, I implemented a small compiler for a language. You
can read about it at www.hi-language.org. The language of the compiler
can be understood to be a cheap Haskell knock-off with ML (eager)
semantics. In short, it is an eager impure functional language with
support for type constructor classes. (I am aware of various ideas
written by mr. Peyton Jones.)

I am looking for people who would like to help met to get the static
semantics right. At the moment, the compiler has been bootstrapped and
has a prototype type-inferencer which discharges type constraints to a
sequent style prover.

Basically, I am looking for people who have done this before and know
more than the average what can be read in various resources so I can
bounce some ideas to them; i.e., people who also know the hairy
details of getting a type system for a programming language right.

I have been asked to make my request more concrete, so, here some of
the background ideas for the intended type inferencer:

1. Support for infinite types.

A lot of straight-forward Hindley-Milner type inferencing algorithms
do not support infinite type whereas they can be very useful. I would
like you to consider the next streaming type as an example for that:
type stream = \i o => i -> (o, stream i o). I'll want infinite types.

2. Support for type annotated records.

The typing system of Haskell is very complex. The Hi language is
designed to be much simpler. More specific, in Haskell the operational
semantics of terms (if I remember correctly) depend on derived
type-dictionaries for terms. In Hi, records are just 'tagged' with
their type constructor, and therefor, the operational semantics do not
depend on the types inferred. This should make type inferencing much
simpler.

3. Support for type classes.

Like in Haskell, types may be instances of type classes, which in Hi
just means that a number of terms become associated with a type
constructor name. I suspect that type inferencing in Hi should be much
easier than in Haskell, and think that a simple system for nominal
typing should be correct, but am not sure.

4. Rethinking of support for existential and universally typed types.

Hi, at the moment, has rudimentary support for the mentioned logical
types. I don't trust these too much as I find those specific types too
much influenced by type theory for logical systems instead of
programming languages. If possible, I would like to get rid of them,
but, at the same time, I don't see a clear alternative. If nothing
else, I'll just stick with them which means that I'll need an
impredicative type system.

5. Getting rid of the sequent calculus prover.

It made sense to use a sequent calculus prover to discharge type
constraints as gathered by the type inferencing process. Basically,
since type checking solely corresponds to proving qualities
(consequences) given a number of assumptions (antecedents) a sequent
prover just seems to be the right choice for type checking.
Unfortunately, such a process comes at a hefty compile-time price.
Such a process is just too heavy weight for checking large pieces of
source code in little time - which is a requirement for most modern
languages. Which means that I would like to have a simpler system
which is just term based. I am not sure this is possible, also given
the fact that I would like to check infinite types, which just goes
best with a sequent style prover.

6. No strange restrictions.

I can't get my head around ML's value restriction and still think
someone must have made a mistake there somewhere. So, if possible,
I'll want a system without these strange added-on patches.

These are all questions I which I am toying with, any hints greatly appreciated.

Thanks for your time,
 M.C.A. (Marco) Devillers