On Mon, 26 Feb 2007 17:28:59 -0800 (PST) [EMAIL PROTECTED] wrote: > The problem with GADTs and other run-time based evidence is just > that: _run-time_ based evidence and pattern-matching. In a non-strict > system, checking that the evidence is really present is the problem on > and of itself.
That's a problem in any system that does not have both termination checking and exhaustive coverage checking. In this presence of both those checks, laziness is not a problem. > BTW, Omega, Dependent ML and a few other systems with > GADTs are strict. Omega does not yet have termination checking AFAIK, and Dependent ML has a more limited type language. Coq does have termination checking, and Neil Mitchell is working on a case-and-termination checker for Haskell. -- Robin _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
