#4116: Type supplement for constructor specific uses of sum types
---------------------------------+------------------------------------------
Reporter: gabrielrf | Owner:
Type: proposal | Status: new
Priority: normal | Component: Compiler
Version: 6.13 | Keywords:
Os: Unknown/Multiple | Testcase:
Architecture: Unknown/Multiple | Failure: None/Unknown
---------------------------------+------------------------------------------
Comment(by 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]
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4116#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
