Dear GHC type hackers, We got a code (please refer to the attached lhs file) that uses type families and type classes very cleverly. We don't know who wrote itbecause this was a contribution of an anonymous reviewer on our paper, which we are still revising. http://kyagrd.dyndns.org/wiki/SharedSubtypes Although we learned a lot from this code, we still have unsolved question about this code.
The problem is, we are still not sure whether this code actually type checks in any GHC version, and we are not even sure whether this should type check or not as it is. I wasn't able to type check this in any of the GHC versions 6.10.1 on windows and debian linux, GHC 6.10.2 on windows and debian linux, or GHC 6.10.3 on debian linux. I also asked some of my colleagues at my school who has GHC installed to run this code, but they weren't able to load up either. However, some people we email conversation with reported that they were able to successfully load this code in GHC version 6.10.1 in their system. This is very surprising because we weren't able to type check it with the same version (GHC 6.10.1) on our machines (Windows XP and Debian Linux). Since there is no reason that GHC type checker would behave differently among different platforms, the code I am attaching is still an unsolved misery to us. It would be very helpful for us if any of can type check this successful could report what version of GHC on what platform and what GHC command line options used to make this code type check. And also, we welcome any discussion whether this code should or should not in principle type check. Thanks in advance, Ahn, Ki Yung FYI, I had the following error message when I tried it on ghc 6.10.3. (When I commented out the problematic line, the last equation of crossB, I was able to load it up though. So, this code definitely doesn't seem to be just thought out of one's mind without actually running on ghc.) ======================================================================== kya...@kyavaio:~/tmp$ ghci --version The Glorious Glasgow Haskell Compilation System, version 6.10.3 kya...@kyavaio:~/tmp$ ghci -fglasgow-exts -XUndecidableInstances Review3.lhs GHCi, version 6.10.3: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer ... linking ... done. Loading package base ... linking ... done. [1 of 1] Compiling Main ( Review3.lhs, interpreted ) Review3.lhs:67:29: Could not deduce (Expandable (Tuple (Map ((,) t2) ys))) from the context (xs ~ t2 ::: ts2, Expandable t2) arising from a use of `:::' at Review3.lhs:67:29-59 Possible fix: add (Expandable (Tuple (Map ((,) t2) ys))) to the context of the constructor `:::' or add an instance declaration for (Expandable (Tuple (Map ((,) t2) ys))) In the expression: Bs (mapB x ys) ::: crossB xs ys In the definition of `crossB': crossB (x ::: xs) ys = Bs (mapB x ys) ::: crossB xs ys In the definition of `expandPair': expandPair _ pair (a ::: as) (b ::: bs) = crossB (a ::: as) (b ::: bs) where crossB :: BList xs -> BList ys -> BList (Cross xs ys) crossB Nil ys = Nil crossB (x ::: xs) ys = Bs (mapB x ys) ::: crossB xs ys mapB :: (Expandable x) => Bit x -> BList ys -> BList (Map ((,) x) ys) mapB x Nil = Nil mapB x (y ::: ys) = pair x y ::: mapB x ys Failed, modules loaded: none.
-------------------- review 3 -------------------- PAPER: 8 TITLE: Functional Pearl: Sparse Bitmaps for Pattern Match Coverage OVERALL RATING: -2 (strong reject) REVIEWER'S CONFIDENCE: 4 (expert) Novelty: 2 (Average) ----------------------- REVIEW -------------------- The paper describes an algorithm for checking pattern match coverage using expandable bit masks. The first half of the paper describes a simply typed version where the types of the pattern are represented as data being passed around. This part is quite good. However, in the second half of the paper a failed attempt is made at reflecting the types of the patterns as Haskell types, allowing matching against polymorphic patterns. This implementation is poorly explained and it seems like the authors haven't fully understood why it isn't working. In fact, it is quite possible to make it work (see below). This could be a very nice paper if the second half were rewritten. Making it work: > type family Expand t > type instance Expand () = Nil > type instance Expand (a, b) = ExpandPair (Expand a) (Expand b) > type instance Expand Bool = () ::: () ::: Nil > type instance Expand (Maybe a) = () ::: a ::: Nil > type instance Expand [a] = () ::: (a, [a]) ::: Nil > type instance Expand (Tuple xs) = xs > type family ExpandPair as bs > type instance ExpandPair as Nil = as > type instance ExpandPair Nil (b ::: bs) = b ::: bs > type instance ExpandPair (a ::: as) (b ::: bs) = Cross (a ::: as) (b ::: bs) > type family Cross as bs > type instance Cross Nil bs = Nil > type instance Cross (a ::: as) bs = Tuple (Map ((,) a) bs) ::: Cross as bs > type family Map (f :: * -> *) xs > type instance Map f Nil = Nil > type instance Map f (x ::: xs) = f x ::: Map f xs > data Tuple xs > data Bit t where > O :: Bit t > I :: Expandable t => Bit t > Bs :: BList (Expand t) -> Bit t > data Nil > data x ::: xs > data BList ts where > Nil :: BList Nil > (:::) :: Expandable t => Bit t -> BList ts -> BList (t ::: ts) > class Expandable t where > expand :: Bit t -> BList (Expand t) > instance (Expandable a, Expandable b) => Expandable (a, b) where > expand (I :: Bit (a, b)) = > expandPair (undefined :: (a, b)) > (\_ _ -> I) (expand (I :: Bit a)) (expand (I :: Bit b)) > expandPair :: forall a b. (Expandable a, Expandable b) => > (a, b) -> -- for unification purposes > (forall x y. (Expandable x, Expandable y) => Bit x -> Bit y -> Bit (x, y)) -> > BList (Expand a) -> BList (Expand b) -> BList (Expand (a, b)) > expandPair _ pair as Nil = as > expandPair _ pair Nil (b ::: bs) = b ::: bs > expandPair _ pair (a ::: as) (b ::: bs) = crossB (a ::: as) (b ::: bs) > where > crossB :: BList xs -> BList ys -> BList (Cross xs ys) > crossB Nil ys = Nil > crossB (x ::: xs) ys = Bs (mapB x ys) ::: crossB xs ys > mapB :: Expandable x => Bit x -> BList ys -> BList (Map ((,) x) ys) > mapB x Nil = Nil > mapB x (y ::: ys) = pair x y ::: mapB x ys > (|*|) :: forall t u. (Expandable t, Expandable u) => Bit t -> Bit u -> Bit (t, u) > O |*| _ = O > _ |*| O = O > I |*| I = I > I |*| Bs ys = case expand (I :: Bit t) of > Nil -> Bs (cast ys) > xs -> Bs xs |*| Bs ys > where > cast :: BList bs -> BList (ExpandPair Nil bs) > cast Nil = Nil > cast (b ::: bs) = b ::: bs > Bs xs |*| I = case expand (I :: Bit u) of > Nil -> Bs xs > ys -> Bs xs |*| Bs ys > Bs xs |*| Bs ys = Bs (expandPair (undefined :: (t, u)) (|*|) xs ys)
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
