[Haskell] Simple IO Regions

[Brandon Moore]

Sean Seefried wrote:
>> Dominic Steinitz wrote:
>>
>>> Can someone give an explanation of how the marks get built up?
>>
>>
>> Suppose we have a class TypeEq a b so that the constraint TypeEq holds
>> whenever a and b are the same. Then the type Int and the type
>>     TypeEq a Int => a
>> are kind of equivalent, right? The HList library plays many tricks
>> like that. The idea is that we can replace a definite type with a type
>> variable subject to some constraint (which we can fix later on).
>> In some respects, constraints are more convenient: they float, their
>> order does not matter, their duplicates are automatically
>> eliminated. Just what we need to build a set...
>> It ``follows'' then that instead of building the union of types, we
>> can build the union of constraints. The latter operation is trivial:
>> the typechecker does that all the time. If we restrict the scope of
>> the type variable by quantification, the scope of the corresponding
>> constraint is likewise restricted. The quantification also builds
>> eigen-variables (which are distinct from anything else) -- so we get
>> 'gensym' on the type level for free. That is all there is to it...
> 
> 
> Olge, I found this explanation really useful. I was wondering if you  
> could explain to me what you mean by eigen-variable though?

I haven't heard the term "eigen-variable" for this before. It makes
great sense in German, from the little I know, but in english it's
mostly a linear algebra term.

The term I've heard is "skolem constant", which is a freshly invented
thing distinct from everything else. I think it's pretty standard usage.
At the very least, that's what Simon Peyton-Jones' uses in his papers on
typechecking Haskell.

A quick summary of the idea is that to check if a term has a quantified
type like forall a . (a -> a), you can invent a new type constant
distinct from everything else in the system, maybe something printed
like A231, and then typecheck the term as if it had the concrete type
A231 -> A231. If it typechecks like that, then you know the code doesn't
require any assumptions about ustated properties of a or its relation to
other types, so it actually does work as forall a . (a -> a).

If the quantifier has a class constraint on it, I think the skolem
constant gets an imaginary instance, for the purpose of typechecking.

Brandon