[Haskell-cafe] Proposal: Sum type branches as extended types (as Type!Constructor)

[Jason Dagit]

On Thu, Jun 3, 2010 at 8:14 AM, Gabriel Riba <griba2001 at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100603/68071070/attachment-0001.html