[Haskell-cafe] Proposal: Sum type branches as extended types (as Type!Constructor)
Extending sum types with data constructors would spare runtime errors or
exception control,
when applying functions to inappropriate branches, as in the example ...
data List a = Nil | Cons a (List a) -- List!Nil and List!Cons
-- as extended types
* Actual system, with runtime errors (as in GHC Data.List head) or
exception throwing
hd :: List a - a
hd (Cons x _) - x
hd Nil - error error: hd: empty list -- error or exception throwing
* Proposed system extending types with constructors as Type!Constructor:
User must do pattern matching before applying the constructor-specific
type function.
In ''var @ (Constructor _ _)'' the compiler should append the constructor
to the type as a pair (Type, Constructor) as an extended type for ''var''
No need for runtime errors or exception control
hd :: List!Cons a - a
hd (Cons x _) = x
using it:
headOf :: List a - Maybe a
headOf list = case list of
li @ (Cons _ _) - Just hd li -- extTypeOf li == ( 'List', 'Cons')
-- should pass typechecker for List!Cons
li @ Nil - Just hd li -- compiler error !!
-- extTypeOf ('List','Nil') don't match
_ - Just hd list -- compiler error !!
-- extTypeOf ('List',Nothing) don't match
Maybe we could take out importance on the number of _ wildcards (constructor
arity) with a syntax like.
li @ (Cons ...)
li @ (Nil ...)
Cheers!
Gabriel Riba Faura.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: Sum type branches as extended types (as Type!Constructor)
On 3 Jun 2010, at 16:14, Gabriel Riba wrote:
Extending sum types with data constructors would spare runtime errors or
exception control,
when applying functions to inappropriate branches, as in the example ...
data List a = Nil | Cons a (List a) -- List!Nil and List!Cons
-- as extended types
* Actual system, with runtime errors (as in GHC Data.List head) or
exception throwing
hd :: List a - a
hd (Cons x _) - x
hd Nil - error error: hd: empty list -- error or exception throwing
* Proposed system extending types with constructors as Type!Constructor:
User must do pattern matching before applying the constructor-specific
type function.
In ''var @ (Constructor _ _)'' the compiler should append the constructor
to the type as a pair (Type, Constructor) as an extended type for ''var''
No need for runtime errors or exception control
hd :: List!Cons a - a
hd (Cons x _) = x
using it:
headOf :: List a - Maybe a
headOf list = case list of
li @ (Cons _ _) - Just hd li -- extTypeOf li == ( 'List', 'Cons')
-- should pass typechecker for List!Cons
li @ Nil - Just hd li -- compiler error !!
-- extTypeOf ('List','Nil') don't match
_ - Just hd list -- compiler error !!
-- extTypeOf ('List',Nothing) don't match
Maybe we could take out importance on the number of _ wildcards (constructor
arity) with a syntax like.
li @ (Cons ...)
li @ (Nil ...)
This looks fairly similar to total functional programming, though putting the
onus on the caller to make sure it meets preconditions, rather than the callee
to make sure it's the right type.
In total functional programming we would say
head :: List a - Maybe a
head (Cons x _) = Just x
head Nil = Nothing
We'd then allow the caller to deal with the maybe any way it likes (commonly
with fmap, or with the maybe function).
Bob___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: Sum type branches as extended types (as Type!Constructor)
On 3 June 2010 16:14, Gabriel Riba griba2...@gmail.com wrote:
Maybe we could take out importance on the number of _ wildcards
(constructor
arity) with a syntax like.
li @ (Cons ...)
li @ (Nil ...)
can't you already use {} to get rid of the underscores?
li@(Cons {})
li@(Nil {})
--
Ozgur Akgun
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: Sum type branches as extended types (as Type!Constructor)
On 06/03/2010 10:14 AM, Gabriel Riba wrote: No need for runtime errors or exception control hd :: List!Cons a - a hd (Cons x _) = x This is already doable using GADTs: data Z data S n data List a n where Nil :: List a Z Cons :: a - List a n - List a (S n) hd :: List a (S n) - a hd (Cons x _) = x tl :: List a (S n) - List a n tl (Cons _ xs) = xs - Jake ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: Sum type branches as extended types (as Type!Constructor)
Jake McArthur wrote: On 06/03/2010 10:14 AM, Gabriel Riba wrote: No need for runtime errors or exception control hd :: List!Cons a - a hd (Cons x _) = x This is already doable using GADTs: data Z data S n data List a n where Nil :: List a Z Cons :: a - List a n - List a (S n) hd :: List a (S n) - a hd (Cons x _) = x tl :: List a (S n) - List a n tl (Cons _ xs) = xs Sure, it is the whipping boy of dependent types afterall. However, * Haskell's standard lists (and Maybe, Either,...) aren't GADTs, * last I heard GADTs are still a ways off from being accepted into haskell', * and, given that this is the whipping boy of dependent types, you may be surprised to learn that pushing the proofs of correctness through for the standard library of list functions is much harder than it may at first appear. Which is why, apparently, there is no standard library for length-indexed lists in Coq.[1] But more to the point, this proposal is different. Gabriel is advocating for a form of refinement types (aka weak-sigma types), not for type families. This is something I've advocated for in the past (under the name of difference types)[2] and am still an avid supporter of-- i.e., I'm willing to contribute to the research and implementation for it, given a collaborator familiar with the GHC code base and given sufficient community interest. The reason why length-indexed lists (and other type families) are surprisingly difficult to work with is because of the need to manipulate the indices in every library function. With refinement types predicated on the head constructor of a value, however, there is no need to maintain this information throughout all functions. You can always get the proof you need exactly when you need it by performing case analysis. The benefit of adding this to the type system is that (a) callees can guarantee that the necessary checks have already been done, thereby improving both correctness and efficiency, and (b) it opens the door for the possibility of moving the witnessing case analysis further away from the use site of the proof. While #b in full generality will ultimately lead to things like type families, there are still a number of important differences. Perhaps foremost is that you needn't define the proof index at the same point where you define the datatype. This is particularly important for adding post-hoc annotations to standard types like lists, Maybe, Either, etc. And a corollary to this is that you needn't settle on a single index for an entire programming community, nor do you impose the cost of multiple indices on users who don't care about them. In short, there's no reason why the equality proofs generated by case analysis should be limited to type equivalences of GADT indices. Value equivalences for ADTs are important too. [1] Though I'm working on one: http://community.haskell.org/~wren/coq/vecs/docs/toc.html [2] http://winterkoninkje.livejournal.com/56979.html -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: Sum type branches as extended types (as Type!Constructor)
On 4 June 2010 03:18, Ozgur Akgun ozgurak...@gmail.com wrote:
On 3 June 2010 16:14, Gabriel Riba griba2...@gmail.com wrote:
Maybe we could take out importance on the number of _ wildcards
(constructor
arity) with a syntax like.
li @ (Cons ...)
li @ (Nil ...)
can't you already use {} to get rid of the underscores?
li@(Cons {})
li@(Nil {})
Even better: you shouldn't need the parentheses:
l...@cons{}
l...@nil{}
--
Ivan Lazar Miljenovic
ivan.miljeno...@gmail.com
IvanMiljenovic.wordpress.com
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: Sum type branches as extended types (as Type!Constructor)
On Thu, Jun 3, 2010 at 8:14 AM, Gabriel Riba griba2...@gmail.com wrote:
Extending sum types with data constructors would spare runtime errors or
exception control,
when applying functions to inappropriate branches, as in the example ...
data List a = Nil | Cons a (List a) -- List!Nil and List!Cons
-- as extended types
* Actual system, with runtime errors (as in GHC Data.List head) or
exception throwing
hd :: List a - a
hd (Cons x _) - x
hd Nil - error error: hd: empty list -- error or exception throwing
* Proposed system extending types with constructors as Type!Constructor:
User must do pattern matching before applying the constructor-specific
type function.
In ''var @ (Constructor _ _)'' the compiler should append the constructor
to the type as a pair (Type, Constructor) as an extended type for ''var''
No need for runtime errors or exception control
hd :: List!Cons a - a
hd (Cons x _) = x
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 define hd for both Cons and Cons2, but not Nil. Do I use an
either type like this?
hd :: Either (List2!Cons a) (List2!Cons2 a) - a
It seems like some other syntax would be desirable here, maybe:
hd :: List2!{Cons, Cons2} a - a
How should it work for functions where no type signature is supplied?
Should it infer the type we would now and only enable the subset of
constructors when the type is explicit as above?
Jason
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
