[Haskell-cafe] Safe lists with GADT's
greenrd at greenrd.org
Mon Feb 26 22:33:21 EST 2007
On Mon, 26 Feb 2007 17:28:59 -0800 (PST)
oleg at pobox.com 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.
More information about the Haskell-Cafe