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

[Thomas Davie]

On 3 Jun 2010, at 16:14, Gabriel Riba 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
> 
> using it:
> 
>   headOf :: List a -> Maybe a
> 
>   headOf list = case list of
> 
>        li @ (Cons _ _) -> Just hd li  -- extTypeOf li == ( 'List', 'Cons')
>                                  -- should pass typechecker for List!Cons
> 
>        li @ Nil  -> Just hd li     -- compiler error !! 
>                                -- extTypeOf ('List','Nil') don't match
> 
>        _ -> Just hd list           -- compiler error !! 
>                                -- extTypeOf ('List',Nothing) don't match
> 
> 
> Maybe we could take out importance on the number of _ wildcards (constructor
> arity) with a syntax like.
>         li @ (Cons ...)
>         li @ (Nil ...)

This looks fairly similar to total functional programming, though putting the onus on the caller to make sure it meets preconditions, rather than the callee to make sure it's the right type.

In total functional programming we would say

head :: List a -> Maybe a
head (Cons x _) = Just x
head Nil = Nothing

We'd then allow the caller to deal with the maybe any way it likes (commonly with fmap, or with the maybe function).

Bob