id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,difficulty,testcase,blockedby,blocking,related
4116,Type supplement for constructor specific uses of sum types,gabrielrf,,"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
",proposal,closed,normal,,Compiler,,invalid,,ozgurakgun@… griba2001@…,Unknown/Multiple,Unknown/Multiple,None/Unknown,,,,,