# [Haskell-cafe] Re: Optimization problem

Ross Paterson ross at soi.city.ac.uk
Tue Sep 19 08:34:40 EDT 2006

```On Tue, Sep 19, 2006 at 01:41:51PM +0200, apfelmus at 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#id3143545

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.

```

More information about the Haskell-Cafe mailing list