[Haskell-cafe] Re: Implementing fixed-sized vectors (using datatype algebra?)

[Alfonso Acosta]

I asked Oleg regarding the use of GADTs to emulate dependent types. My
conclusion is that I should forget about them. Here is the full
answer:


---------- Forwarded message ----------
From:  <oleg at okmij.org>
Date: Feb 12, 2008 8:49 AM
Subject: Re: GADTs to emulate dependent types?
To: alfonso.acosta at gmail.com



Hello!

> The main question is whether it is feasible to use GADTs to define
> fixed-sized vectors or not. The motivation behind it is to avoid
> needing to code your own trusted core and use the compiler typechecker
> for that purpose instead.

That is a false proposition. In Haskell, any code that uses GADT
*MUST* use a run-time test (run-time pattern match). Otherwise, the
code is unsound and provides no guarantees. The particular value of a
GADT data type is a witness of a proposition expressed in the type of
GADT (e.g., type equality). Since it is possible in Haskell to fake
this witness (just write undefined), if you don't check the witness at
run-time, that is, test that the witness is a real value rather than
undefined, you don't get any guarantees. That is why the irrefutable
pattern-match does not work with GADT. Incidentally, the first
implementation of GADT in GHC did permit irrefutable pattern-match,
which did let one write unsound code (that is, code that gave
segmentation fault):
       http://okmij.org/ftp/Haskell/GADT-problem.hs

The issue is not present in Coq, for example, whose core calculus is
sound and you cannot fake the evidence.

Thus, the unsoundness of Haskell (the presence of undefined) mandates
the run-time test for any code that uses GADT. So, GADTs are
fundamentally less efficient than the typeclasses; the latter can
provide assurances that can be checked at compile-time only, with no
run-time artifacts.

> data FSVec :: * -> * -> * where
>     NullV :: FSVec D0 a
>     (:>)  :: Succ s s' => a -> FSVec s a -> FSVec s' a

That is an old problem, and a difficult problem. In Singapore I was
talking to Zhaohui Luo (you can look him up on Google), who said that
the problem of asserting two types being equal (that is,
Succ D0 being equal to D1) is a very tough one. Conor McBride have
written a paper on observational equality -- but this is not
Haskell. So, I don't think this approach works.

       Cheers,
       Oleg