[Haskell-cafe] Re: Optimization problem
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:
See the second restriction. Irrefutable patterns aren't mentioned
there, but they're the general case. See also
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 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