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: