[Haskell-cafe] Safe lists with GADT's

[Robin Green]

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.

-- 
Robin