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 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
programs (by creating a proof interactively) but these seem
orthogonal to the actual type system itself.
Also, typing is not the only issue for compile time guarantees.
Consider:
data Dir = Left | Right | Up | Down deriving Eq
-- Compiler can check the function is total
foo :: Dir -> String
foo Left = "Horizontal"
foo Right = "Horizontal"
foo Up = "Vertical"
foo Down = "Vertical"
versus
-- Less verbose but compiler can't look inside guards
foo x | x == Left || x == Right = "Horizontal"
foo x | x == Up || x == Down = "Vertical"
versus something like:
foo (Left || Right) = ...
foo (Up || Down) = ...
Brian.
--
http://www.metamilk.com
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
