Stronger static types, was Re: [Haskell-cafe] Re: Versioning

[Brian Hulley]

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