#4116: Type supplement for constructor specific uses of sum types
---------------------------------+------------------------------------------
Reporter: gabrielrf | Owner:
Type: proposal | Status: new
Priority: normal | Milestone:
Component: Compiler | Version:
Keywords: | Difficulty:
Os: Unknown/Multiple | Testcase:
Architecture: Unknown/Multiple | Failure: None/Unknown
---------------------------------+------------------------------------------
Description changed by igloo:
Old description:
> 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
New description:
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:12>
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
