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 ------------------ _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe Diag.lhs (3K) Download Attachment |
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. 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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe signature.asc (196 bytes) Download Attachment |
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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Free forum by Nabble | Edit this page |