[Haskell-cafe] Re: Optimization problem

[Ross Paterson]

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.