Type supplement for constructor specific uses of sum types

Benefits: Avoid error calls (runtime), exception control and Maybe types in partially defined (constructor specific) functions on sum types

Method: by refining function argument types with a list of constructors applyable and detecting the target constructor at the caller through pattern matching, flagging with compiler errors the unmatched cases.

As an example, with

data List a = Nil | Cons a (List a)

• Actual system: undefined cases are discriminated with runtime errors or

exception throwing or optional Maybe results.

   hd :: List a -> a
   hd (Cons x _) -> x
   hd Nil -> error "error: hd: empty list" -- (as in GHC Data.List head)

• Proposed system: supplement types with

a suffix @Constructor or @{Constructor1, Constructor2}

denoting the list of constructors to which the function can be applied.

   hd :: List @Cons a -> a
   hd (Cons x _) = x

   -- no definition for unappropriate constructors.

The caller must do pattern matching before applying the constructor-specific function.

In a pattern var @ (Constructor {}) the compiler should set a constructorAt property for var to the specified pattern constructor and when used in a constructor specific parameter position match the type supplement constructor list

using it:

   accumulateHead :: (a->b) -> a -> List a -> b

   accumulateHead f accum list = case list of

        li @ Cons {} -> f accum $ hd li  -- constructorAt li == 'Cons'
                              -- should pass typechecker at ''hd'' for ''List @ Cons''

        li @ Nil  -> f accum $ hd li     -- compiler error !! 
                                -- constructorAt li == 'Nil' ; no match

        _ -> f accum $ hd list           -- compiler error !! 
                                -- constructorAt list == Nothing ; no match

        _ -> accum       -- default option closing pattern matching exhaustivity.

(from Jason Dagit contribution)

Syntax {Cons, Cons2} for more than one constructor

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

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

Discussion thread:

http://thread.gmane.org/gmane.comp.lang.haskell.cafe/75586