Hello,
It seems likely that you have the uses for the inferred type of the above
expression other than displaying it. You probably want to statically enforce
certain constraints when applying these Lam expressions. That is, you
want to apply Lam expressions only to the arguments that satisfy the
inferred HasField constraints. Why not to enforce the constraints at
that time then? The enclosed is a bit simplified version of the
code that demonstrates the idea. It is the typed evaluator statically
enforcing the HasField constraints. It does not use GADTs though as
they don't add to expressiveness. It would be great if we could delay
the more detailed discussion past the first week of Jan.
Thanks for the response. Don't worry about responding back quickly. I
wanted to give a quick response in order to give a better idea of what
I'm trying to do.
I am not intending to evaluate the expressions I'm creating. I really
want Haskell to typecheck the expressions for me-- that is, I want to
use the Haskell typechecker to statically typecheck my expressions
(the intended use of this is to generate code). In a sense, your
sample code bypasses the interesting/hard/troublesome part by not
descending into the body of the Lam.
Of course, using higher-order abstract syntax would be trivial if
Haskell's type system coincided with that of the object language. On
the other hand, HOAS tends to not work if the meta language doesn't
match the object language. My intuition, mostly due to your work, is
that Haskell's type class system can be used to effectively extend
Haskell's type system; and I wanted to see if that would allow for a
HOAS encoding of a language with a type system which doesn't match
Haskell's.
> and TypeEq doesn't work on uninstantiated type vars; correct me if I'm
> wrong about these.
TypeEq may work on uninstantiated type vars; please see
http://pobox.com/~oleg/ftp/Haskell/de-typechecker.lhs
and the paragraph containing the phrase ``The ability to operate on
and compare *unground* types with *uninstantiated* type variables is
often sought but rarely attained. The contribution of this message is
the set of primitives for nominal equality comparison and
deconstruction of unground types.''
I will take a closer look at this.
thanks,
Jeff
_______________________________________________
Haskell mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell
