Inlining and generic programming
Simon Peyton-Jones
simonpj at microsoft.com
Fri Mar 9 18:49:43 CET 2012
Pedro
The second part of your message (attached), about generics, turned out to be *much* more subtle. You wondered why it made a difference whether you said
instance GEnum Nat where
genum = map to genum'
or
instance GEnum Nat -- Fill in from default method
Well, it turns out that the difference is largely accidental. Here are the types of the functions involved:
to :: Representable a => Rep a -> a
genum' :: GEnum' a => [a]
type instance Rep Nat = RepNat
type RepNat = U :+: (Rec Nat)
Consider the instance definition
genum = map to genum'
There are two different ways of typing it:
(A) map @RepNat @Nat (to @Nat dReprNat |> g1) (genum' @RepNat dGEnum'_RepNat)
where
g1 :: Rep Nat -> Nat ~ RepNat -> Nat
dReprNat :: Representable Nat
dGEnum'Nat :: GEnum' RepNat
or
(B) map @(Rep Nat) @Nat (to @Nat dReprNat) (genum' @(Rep Nat) dGEnum'_Rep_Nat)
where
dReprNat :: Representable Nat
dGEnum'Nat :: GEnum' (Rep Nat)
Which of these is chosen depends on accidental things in the constraint solver; it's not supposed to matter.
But it DOES affect whether the map/(|||) rule fires.
{-# RULES "ft |||" forall f a b. map f (a ||| b) = map f a ||| map f b #-}
It makes a difference because in (A) we have an instance for GEnum' RepNat that uses ||| directly,
instance (GEnum' f, GEnum' g) => GEnum' (f :+: g) where
genum' = map L genum' ||| map R genum'
so we get
map ... (blah1 ||| blah2)
But in (B) we need an instance for GEnum' (Rep Nat) and that has an extra cast, so we get
map ... ((blah1 ||| blah2) |> g)
And the cast stops the RULE for map/(|||) firing.
=============== Parametricity to the rescue =============
Note that (|||) :: [a] -> [a] -> [a]
So by parametricity we know that
if g :: [T1] ~ [T2]
then
((|||) @T1 xs ys |> g)
=
((|||) @T2 (xs |> g) (ys |> g)
If we used that to push the cast inwards, the RULE would match.
Likewise, map is polymorphic: map :: (a->b) -> [a] -> [b]
So by parametricity
if :: [T1] -> [T2]
then
map @T2 @TR f (xs |> g)]
=
map @T1 @TR (f |> sym (right g) -> TR) xs
If we used that to move the cast out of the way, the RULE would match too.
But GHC is nowhere near clever enough to do either of these things. And it's far from obvious what to do in general.
=================
Bottom line: the choices made by the constraint solver can affect exactly where casts are inserted into the code. GHC knows how to move casts around to stop them getting in the way of its own transformations, but is helpless if they get in the way of RULES.
I am really not sure how to deal with this. But it is very interesting!
Simon
-------------- next part --------------
An embedded message was scrubbed...
From: =?iso-8859-1?Q?Jos=E9_Pedro_Magalh=E3es?= <jpm at cs.uu.nl>
Subject: Inlining and generic programming
Date: Wed, 22 Feb 2012 14:32:32 +0000
Size: 63524
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120309/c302bbcf/attachment-0001.eml>
More information about the Glasgow-haskell-users
mailing list