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