[jhc] explanation of FrontEnd.KindInfer.constrain

[John Meacham]

On Tue, Mar 18, 2008 at 06:37:29PM -0400, Samuel Bronson wrote:
> On 3/18/08, John Meacham <john at repetae.net> wrote:
> > On Tue, Mar 18, 2008 at 06:09:22PM -0400, Samuel Bronson wrote:
> > > I don't understand how FrontEnd.KindInfer.constrain is supposed to
> > > deal with KindSimple constraints... it doesn't seem to have any way of
> > > replacing ?? or ? with *. Why not?
> >
> > that is done in the FrontEnd.Tc.Kind.kindCombine routine. The kind
> > inference algorithm is based on the impredicative boxy type inferencer
> > used as the main typechecker.  this is because jhc is going to be a
> > kind-polymorphic system, much like the Omega language (based on
> > haskell). That and I find the impredicative boxy typechecking algorithm
> > quite elegant. And when my moratorium on adding new features ends, I
> > want to finish support for bang kinds. so,
> >
> > data List a = Cons a (List a) | Nil
> >
> > will actualy declary a type of
> >
> > List :: forall (k1::**) (k2::**) . \(a::k2) -> k1
> >
> > (** is the supersort of boxed (but not necessarily lazy) values.
> >
> > this means you can have
> >
> > List * * - lazy list of lazy elements
> > List ! * - strict list of lazy elements
> > List * ! - lazy list of strict elements
> > List ! ! - strict list of strict elements
> 
> So what is KindInfer.constrain for, then?

'constrain' refines a type subject to constraints, kindCombine actually
returns what the unification of the kinds are. constrain works on
constraints, combine works on kinds. constraints don't necessarily map
to kinds, though currently most have an analog.

        John

-- 
John Meacham - ⑆repetae.net⑆john⑈