[jhc] explanation of FrontEnd.KindInfer.constrain

[John Meacham]

On Wed, Mar 19, 2008 at 06:21:45PM -0400, Samuel Bronson wrote:
> On 3/18/08, Samuel Bronson <naesten at gmail.com> wrote:
> > On 3/18/08, John Meacham <john at repetae.net> wrote:
> > > On Tue, Mar 18, 2008 at 06:52:04PM -0400, Samuel Bronson wrote:
> > > > On 3/18/08, John Meacham <john at repetae.net> wrote:
> > > >
> > > > > '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.
> > > >
> > > > Eh? Doesn't KindInfer run before typechecking begins?
> > >
> > > excuse me, I meant 'kind', not 'type'. this terminology is real
> > > trickylike... At least I made sure that jhc core's axioms allowed a
> > > stratified type system so 'term','type','kind','superkind' all are
> > > distinct sets and have no cyclic dependencies... though, I am not sure
> > > if there are practical languages where that is not the case.. though
> > > wacky type systems are fun to play with.
> >
> > Well, it seems like constrain doesn't really have any choice but to
> > throw an error when asked to constrain a KBase KQuest with a
> > KindSimple constraint... it has no way of indicating that the result
> > should be a KBase KStar!
> 
> I was hoping you might have something to say about this?

Ah, sorry. I was mulling it over. Basically, it has to do with the issue
that '?' and '??' are not real kinds. they are just shorthand for kind
abstractions.

when you say:
data App :: ?? -> ? -> *

you actually mean:

(in psuedo-haskell)

data App :: 
        forall (k1 | k1 `elem` [*,#]) (k2 | k2 `elem` [*,#,(#)]) . k1 -> k2 -> *

the constraints are what is to the right of the |'s there. (I could also
do this with superkinds, though I think constrained polymorphism is the
way to go here.).

so, ? should not actually be a kind of type '?' but actually a newly
instantiated kind variable with a KindQuest constraint on it. This
instantiation should be done whenever we pull something out of the kind
environment. 

However, since full kind polymorphism isn't availibe in the front end,
we use ? and ?? as placeholders in our code as well as data structures.

they actually behave the same as if they had been declared:

kindsynonym ?? = exists k | k `elem` [*,#] . k


Right now, for compatability with haskell 98 and because I would need to
modify some data structures to handle it, we perform a 'defaulting',
defaulting all kindvars to * at the end of inference. we could just as
easily perform a generalization there and get true kind polymorphism.
(and this will be done eventually)

note that type synonyms are already kind polymorphic:

type UIO a = World__ -> (# World__, a #)

'UIO Int' and 'UIO Bits32_' are both fine.

UIO :: forall k . k -> *

(actually, to be fully formal, UIO has superkind polymorhism, but that
is irrelevant since type synonyms don't make it to jhc core, jhc can
handle that fine, but I think I will wait until 'kind level' programming
becomes popular before crossing that bridge :) )


so. to answer the question of why that case dealing with KQuest isn't in
constrain, it is either because

1. I forgot it, it actually should be there.

or 

2. an actual '?' or '??' is sneaking in as a kind when it should have
been turned into a freshly instantiated kind variable with a ? or ??
constraint as appropriate.

as an aside, it is interesting to note that methodless type classes give
a sort of constrained polymorphism at the type level, I am not sure the
signifigance exactly of this, but it might lead to a more elegant
handling of kinds in the future... uncharted waters. 

        John





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