[Haskell] Re: Even higher-order abstract syntax: typeclasses vs GADT

[oleg at pobox.com]

Benjamin Franksen wrote:
> I would be interested whether you can not only /check/ well-typedness,
> but also /establish/ it, i.e. is it possible to have the input to the
> type-checker be an /untyped/ representation (such as obtained by
> parsing a program in text form) and the output be a typed one (or else
> a type error)?

The original problem was to embed a domain-specific term language in
Haskell and get the Haskell typechecker to flag meaningless terms when
compiling code files. You, as I understand it, would like to do the
same for terms read, at run-time, from files or received from
(remote) sources. Right? Well, it seems that's where staging/TH can be
useful. Rather then writing
	badfoo = Fix id
in the source code, we can write
	badfoo = $(read_the_Foo_term "from-file")
The typechecking will be performed by TH. It seems we have discussed
that before:
  http://www.haskell.org/pipermail/haskell-cafe/2006-November/019193.html
That article contains the complete working example.

I think Alice developers can say quite a bit about this problem of
type-safe pickling and especially unpickling.

Perhaps we should move to Cafe?