[EMAIL PROTECTED] 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 _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell