[jhc] explanation of FrontEnd.KindInfer.constrain
john at repetae.net
Wed Mar 19 18:48:30 EDT 2008
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
when you say:
data App :: ?? -> ? -> *
you actually mean:
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
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.
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 Meacham - ⑆repetae.net⑆john⑈
More information about the jhc