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

[Benjamin Franksen]

oleg at pobox.com wrote:
> We show the typeclass implementation of the example used to make the
> case for GADTs. We demonstrate the higher-order abstract-syntax-based
> embedding of a language in Haskell and implement static and dynamic
> semantics of the language. The interpreter of the language is tagless
> and statically assured: Only well-typed terms may be evaluated, and
> the evaluation of those does not get stuck. We use no tags and *no*
> run-time pattern-matching, therefore, the `eval' function has no
> possibility of raising a run-time error.  Our language is
> _non_-strongly normalizing and non-structurally inductive due to the
> presence of Fix; yet the typechecking is decidable and our typeclass
> programs always terminate.

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)?

>From my very limited understanding of these issues I would say it is not
possible, neither with type-classes nor with G[AR]DTs because it would mean
the return type of the function 'typecheck' would have to vary depending on
the input data, hence you'd need a genuinely dependent type system for such
a feat. (However, I am not nearly expert enough to make more than a half
educated guess here, hence posing this as a question rather than a
statement).

Cheers
Ben