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:
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