[jhc] explanation of FrontEnd.KindInfer.constrain

[Samuel Bronson]

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?