oleg@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