On Tue, Sep 19, 2006 at 01:41:51PM +0200, apfelmus@quantentunnel.de wrote:
Btw, why are there no irrefutable patterns for GADTs?
Not GADTs, but existential types (whether done with GADTs or not). They can't be analysed with irrefutable patterns, of which let bindings are a special case: http://www.haskell.org/ghc/docs/6.4.2/html/users_guide/type-extensions.html#... See the second restriction. Irrefutable patterns aren't mentioned there, but they're the general case. See also http://www.haskell.org/pipermail/haskell-cafe/2006-May/015609.html http://www.haskell.org/pipermail/glasgow-haskell-users/2006-May/010278.html though I don't buy the rationale there. Hugs has no such restriction.
I mean, such a sin should be shame for a non-strict language...
It certainly bites in this case. We could define data TLeaf data TNode s1 s2 data MapShape s k where SLeaf :: MapShape TLeaf k SNode :: !Int -> k -> MapShape s1 k -> MapShape s2 k -> MapShape (TNode s1 s2) k data MapData s a where DLeaf :: MapData TLeaf a DNode :: a -> MapData s1 a -> MapData s2 a -> MapData (TNode s1 s2) a data InsertResult s k = forall s'. InsertResult (MapShape s' k) (forall a. MapData s' a -> (a, MapData s a)) insert :: Ord k => k -> MapShape s k -> InsertResult s k and have the compiler check that the transformations on the shape match the transformations on the data, but first we need to turn lots of lets into cases and erase the tildes. Of course the resulting program no longer works, but it does have verifiably correct transformations.