Re: [Haskell] Simple IO Regions
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? Sean
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
participants (2)
-
Brandon Moore -
Sean Seefried