Gabriel Riba wrote:
New proposal draft:
Proposal: Type supplement for constructor specific uses of sum types
Purpose: Avoid error clauses (runtime errors), exception control or Maybe
types in partially defined (constructor specific) functions on sum types.
As an example, with
data List a
Jason Dagit dagit at codersbase.com writes:
How will this proposal scale with data types that have multiple
alternatives that make sense? No natural examples come to mind
so how about a contrived example:
data List2 a = Nil | Cons a (List2 a) | Cons2 a a (List2 a)
Now I want to
Edward Kmett suggests the use of @ instead of !
Edward Kmett wrote:
This is just a form of refinement type. Googling the term should turn up a
couple dozen papers on the topic.
You can emulate them (and more) with phantom types in the existing
type system, though admittedly the encoding is
