Does this, and should this type check on GHC 6.10.x ?

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.) ======================================================================== kyagrd@kyavaio:~/tmp$ ghci --version The Glorious Glasgow Haskell Compilation System, version 6.10.3 kyagrd@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.

On Jun 26, 2009, at 00:47 , Ahn, Ki Yung wrote:
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
I'm under the impression that many clever uses of type families require GHC HEAD, as they're still evolving. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH

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.
Have you first, before you turn to GHC< considered whether this code should be well-typed in any type system?
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
At first sight, it looks like this constraint Expandable (Tuple (Map ((,) t2) ys)) is indeed one that's required to hold in order to make the code well-typed. Do you agree? Yet I see no instance of Expandable for Tuple. So why do you think this constraint should hold anyway? Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be url: http://www.cs.kuleuven.be/~toms/ Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm
participants (3)
-
Ahn, Ki Yung
-
Brandon S. Allbery KF8NH
-
Tom Schrijvers