[weird stuff] The Dodgy Diagonal
Scary words warning: Polynomial, Functor, Bifunctor, unsafeCoerce# Folks A peculiar query for folks who know more about the internals of Haskell compilers than I do. I attach the full code with all the bits and pieces, but let me pull out the essentials in order to state the problem. I've been mucking around with polynomial types in one parameter
newtype Id x = Id x -- element newtype K1 a x = K1 a -- constant data ((Sum1 p q)) x = L1 (p x) | R1 (q x) -- choice data ((Prod1 p q)) x = P1 (p x) (q x) -- pairing
all of which give unremarkable instances of Functor < class Functor p where < fmap :: (s -> t) -> p s -> p t
instance Functor Id instance Functor (K1 a) instance (Functor p, Functor q) => Functor (Sum1 p q) instance (Functor p, Functor q) => Functor (Prod1 p q)
I've also been mucking around with polynomial types in two parameters
newtype Fst x y = Fst x newtype Snd x y = Snd y newtype K2 a x y = K2 a data ((Sum2 p q)) x y = L2 (p x y) | R2 (q x y) data ((Prod2 p q)) x y = P2 (p x y) (q x y)
which give unremarkable bifunctors, doing two maps at once
class Bifunctor p where bimap :: (s1 -> t1) -> (s2 -> t2) -> p s1 s2 -> p t1 t2
instance Bifunctor Fst where bimap f g (Fst x) = Fst (f x)
instance Bifunctor Snd where bimap f g (Snd y) = Snd (g y)
instance Bifunctor (K2 a) instance (Bifunctor p, Bifunctor q) => Bifunctor (Sum2 p q) instance (Bifunctor p, Bifunctor q) => Bifunctor (Prod2 p q)
Now, I'm interested in collapsing the diagonal. What? Er, this:
class (Bifunctor b, Functor f) => Diag b f | b -> f where diag :: b x x -> f x gaid :: f x -> b x x
If the two parameters to a bifunctor are instantiated with the same thing, we should be able to exchange with the functorial representation. I'll just do one way.
instance Diag Fst Id where diag (Fst x) = Id x
instance Diag Snd Id where diag (Snd x) = Id x
instance Diag (K2 a) (K1 a) where diag (K2 a) = K1 a
instance (Diag pb pf, Diag qb qf) => Diag (Sum2 pb qb) (Sum1 pf qf) where diag (L2 p) = L1 (diag p) diag (R2 q) = R1 (diag q)
instance (Diag pb pf, Diag qb qf) => Diag (Prod2 pb qb) (Prod1 pf qf) where diag (P2 p q) = P1 (diag p) (diag q)
That looks like a whole lot of doing very little. So, can I (in practice, in this or that compiler) get away with...
dodgy :: Diag b f => b x x -> f x dodgy = unsafeCoerce#
ygdod :: Diag b f => f x -> b x x ygdod = unsafeCoerce#
...dodgy for diag and ygdod for giad? Minimal nontrivial experiments in ghc give grounds for cautious optimism, but I'd be delighted to hear from better informed sources. Cheers Conor ------------------
On Sat, Jul 14, 2007 at 12:06:30PM +0100, Conor McBride wrote:
A peculiar query for folks who know more about the internals of Haskell compilers than I do. I attach the full code with all the bits and pieces, but let me pull out the essentials in order to state the problem.
newtype Id x = Id x -- element newtype K1 a x = K1 a -- constant data ((Sum1 p q)) x = L1 (p x) | R1 (q x) -- choice data ((Prod1 p q)) x = P1 (p x) (q x) -- pairing
newtype Fst x y = Fst x newtype Snd x y = Snd y newtype K2 a x y = K2 a data ((Sum2 p q)) x y = L2 (p x y) | R2 (q x y) data ((Prod2 p q)) x y = P2 (p x y) (q x y)
class (Bifunctor b, Functor f) => Diag b f | b -> f where diag :: b x x -> f x gaid :: f x -> b x x
instance Diag Fst Id where instance Diag Snd Id where instance Diag (K2 a) (K1 a) where instance (Diag pb pf, Diag qb qf) => Diag (Sum2 pb qb) (Sum1 pf qf) where instance (Diag pb pf, Diag qb qf) => Diag (Prod2 pb qb) (Prod1 pf qf)
That looks like a whole lot of doing very little. So, can I (in practice, in this or that compiler) get away with...
dodgy :: Diag b f => b x x -> f x dodgy = unsafeCoerce#
ygdod :: Diag b f => f x -> b x x ygdod = unsafeCoerce#
...dodgy for diag and ygdod for giad?
Minimal nontrivial experiments in ghc give grounds for cautious optimism, but I'd be delighted to hear from better informed sources.
In GHC 6.7.20070712 and Yhc, this is perfectly safe. The "ABI" GHC uses for data types is determined only by the number of constructors and the number of pointer and non-pointer arguments to each constructor; so your pairs of values are compatible. Case analysis is done in these systems by examining a small integer pointed to from the tag pointer, so identically-shaped data types will have identical small integers ======== module X where data X a b = Y a | Z a moo z = case z of Z a -> a ; Y a -> a ======== A fragment of the asm output, rearranged and commented: X_moo_info: ; Enter here. EBP is the stack pointer, z is ; on the stack, as is a return address. movl (%ebp),%esi ; Load z into ESI, which the standard calling ; convention uses for the pointer to the object ; under evaluation. movl $s80_info,(%ebp) ; Store a return address, so that we can ; evaluate z. Appears to re-use the stack space ; required for the z argument jmp *(%esi) ; Jump to z's evaluation code s80_info: ; z is evaluated now; the result of evaluation ; is in ESI. movl (%esi),%eax ; Fetch the raw tag of the value cmpw $1,-2(%eax) ; -2(%eax) fetches the small integer associated ; with the tag. Compare it to 1. jae .Lc8g ; degenerate decisiontree switch movl 4(%esi),%esi ; Load the field of the evaluated constructor addl $4,%ebp ; Clean up the stack jmp stg_ap_0_fast ; Returning evals are tricky. Jump to common ; RTS code .Lc8g: ; same as before movl 4(%esi),%esi addl $4,%ebp jmp stg_ap_0_fast In GRIN based systems like Jhc, this is *not* safe, since after evaluation comparisons are done using the full tag. ====== {-# OPTIONS_JHC --noprelude #-} -- compiling the prelude would take days, I'm not going to wait module Main where import Jhc.Prim import Jhc.Basics import Jhc.Monad data X1 a b = Y1 a | Z1 a data X2 a b = Y2 a | Z2 a main = case (unsafeCoerce__ (Z2 ())) of Y1 _ -> putStrLn "No" Z1 _ -> putStrLn "Yes" putChar :: Char -> IO () putChar c = c_putwchar (ord c) foreign import ccall "stdio.h jhc_utf8_putchar" c_putwchar :: Int -> IO () putStr :: String -> IO () putStr s = mapM_ putChar s putStrLn :: String -> IO () putStrLn s = do putStr s putChar '\n' ===== stefan@stefans:/usr/local/src/jhc$ ./hs.out match falls off bottom: Main.Z2 () I don't know enough about nhc, hbc, yale-haskell, or Hugs to answer for them. Stefan
Hi Stefan Thanks for a very enlightening reply.
In GHC 6.7.20070712 and Yhc, this is perfectly safe.
In GRIN based systems like Jhc, this is *not* safe, since after evaluation comparisons are done using the full tag.
It's now occurred to me that at a cost of some noise, I could have done things a little differently On 14 Jul 2007, at 20:37, Stefan O'Rear wrote:
On Sat, Jul 14, 2007 at 12:06:30PM +0100, Conor McBride wrote:
A peculiar query for folks who know more about the internals of Haskell compilers than I do. I attach the full code with all the bits and pieces, but let me pull out the essentials in order to state the problem.
newtype Id x = Id x -- element newtype K1 a x = K1 a -- constant
newtype Up1 f p q x = U1 (f (p x) (q x)) type Sum1 = Up1 Either type Prod1 = Up1 (,)
newtype Fst x y = Fst x newtype Snd x y = Snd y newtype K2 a x y = K2 a
newtype Up2 f p q x y = U2 (f (p x y) (q x y)) type Sum2 = Up2 Either type Prod2 = Up2 (,)
class (Bifunctor b, Functor f) => Diag b f | b -> f where diag :: b x x -> f x gaid :: f x -> b x x
and then all of my coercions would (recursively) have been between newtype-isotopes. Would that have more universal traction? I realise, of course that it's all voodoo, and I shouldn't trust a thing. Cheers Conor
ctm:
Hi Stefan
Thanks for a very enlightening reply.
In GHC 6.7.20070712 and Yhc, this is perfectly safe.
In GRIN based systems like Jhc, this is *not* safe, since after evaluation comparisons are done using the full tag.
It's now occurred to me that at a cost of some noise, I could have done things a little differently
On 14 Jul 2007, at 20:37, Stefan O'Rear wrote:
On Sat, Jul 14, 2007 at 12:06:30PM +0100, Conor McBride wrote:
A peculiar query for folks who know more about the internals of Haskell compilers than I do. I attach the full code with all the bits and pieces, but let me pull out the essentials in order to state the problem.
newtype Id x = Id x -- element newtype K1 a x = K1 a -- constant
newtype Up1 f p q x = U1 (f (p x) (q x)) type Sum1 = Up1 Either type Prod1 = Up1 (,)
newtype Fst x y = Fst x newtype Snd x y = Snd y newtype K2 a x y = K2 a
newtype Up2 f p q x y = U2 (f (p x y) (q x y)) type Sum2 = Up2 Either type Prod2 = Up2 (,)
class (Bifunctor b, Functor f) => Diag b f | b -> f where diag :: b x x -> f x gaid :: f x -> b x x
and then all of my coercions would (recursively) have been between newtype-isotopes.
Would that have more universal traction? I realise, of course that it's all voodoo, and I shouldn't trust a thing.
I do wonder if there's some type families/associated type/witness games that could be played here. Any thoughts on that, Conor? http://haskell.org/haskellwiki/GHC/Indexed_types -- Don
participants (4)
-
Conor McBride -
Conor McBride
-
dons＠cse.unsw.edu.au -
Stefan O'Rear