On Thu, Jun 3, 2010 at 8:14 AM, Gabriel Riba <griba2001@gmail.com> wrote:

Extending sum types with data constructors would spare runtime errors or
exception control,

when applying functions to inappropriate branches, as in the example ...

data List a = Nil | Cons a (List a) -- List!Nil and List!Cons
-- as extended types

* Actual system, with runtime errors (as in GHC Data.List head) or
exception throwing

hd :: List a -> a
hd (Cons x _) -> x
hd Nil -> error "error: hd: empty list" -- error or exception throwing

* Proposed system extending types with constructors as Type!Constructor:

User must do pattern matching before applying the constructor-specific
type function.

In ''var @ (Constructor _ _)'' the compiler should append the constructor
to the type as a pair (Type, Constructor) as an extended type for ''var''

No need for runtime errors or exception control

hd :: List!Cons a -> a

hd (Cons x _) = x

How will this proposal scale with data types that have multiple alternatives that make sense? No natural examples come to mind so how about a contrived example:

data List2 a = Nil | Cons a (List2 a) | Cons2 a a (List2 a)

Now I want to define hd for both Cons and Cons2, but not Nil. Do I use an either type like this?

hd :: Either (List2!Cons a) (List2!Cons2 a) -> a

It seems like some other syntax would be desirable here, maybe:

hd :: List2!{Cons, Cons2} a -> a

How should it work for functions where no type signature is supplied? Should it infer the type we would now and only enable the subset of constructors when the type is explicit as above?

Jason