Brian Hulley wrote:
Would it be possible to augment Haskell's type system so that it was
the same as that used in Epigram?
No, no! Epigram is a wonderfully pure research experiment in one corner
of the design space. The corner it is exploring is not particularly
"Haskell like", though the r
Yes, Bluespec has efficient type level naturals. But it only has
arithmetic and some trivial decision procedures. The slogan is "the
type checker knows arithmetic, not algebra".
It worked pretty well. But you soon get into situations where you
need polymorphic recursion of functions with t
On Dec 21, 2006, at 5:03 PM, Jacques Carette wrote:
...
What must be remembered is that full dependent types are NOT needed
to get a lot of the benefits of dependent-like types. This is what
some of Oleg's type gymnastics shows (and others too). My interest
right now lies in figuring ou
It's possible to augment Haskell type system to be the one in
Epigram. But it would no longer be Haskell. :) And to meet the
goals of Epigram you'd also have to remove (unrestricted) recursion
from Haskell.
-- Lennart
On Dec 21, 2006, at 23:46 , Brian Hulley wrote:
Jacques Care
Jacques Carette wrote:
Yes, dependent types have a lot to do with all this. And I am an
eager lurker of all this Epigram.
Would it be possible to augment Haskell's type system so that it was the
same as that used in Epigram?
Epigram itself uses a novel 2d layout and a novel way of writing pro
Yes, dependent types have a lot to do with all this. And I am an eager
lurker of all this Epigram.
Scott Brickner wrote:
Jacques Carette wrote:
Array out-of-bounds, fromJust, head on an empty list, and
pattern-match failures are in my list of things I wish the type
system could help me with.
