On 2004-08-31T09:55:10-0700, Lyle Kopnicky wrote:
Sorry, I don't think I made myself clear. I'm not defining PI, it's the standard type binding operator, like lambda is the variable binding operator. Maybe I could write it as 'II' so it looks more like a capital pi. It's not a feature of Haskell, but part of type theory (dependent types). I was mixing and matching and making it look like Haskell. So instead of 'PI r -> ContT r m', I could write 'flip ContT', except that 'flip' needs to work on a type level instead of a value level. Or I could write '(`ContT` m)', or 'ContT _ m', where the '_' is a hole. Does this make sense now?
Yes, it makes sense now. You need to define newtype FlipContT m r a = FlipContT (ContT r m a) or more generally, newtype Flip c (m :: * -> *) r a = Flip (c r m a) The rationale for disallowing matching partially-applied type synonyms is that higher-order unification is undecidable. See also: Neubauer, Matthias, and Peter Thiemann. 2002. Type classes with more higher-order polymorphism. In ICFP '02: Proceedings of the ACM international conference on functional programming. New York: ACM Press. http://www.informatik.uni-freiburg.de/~neubauer/papers/icfp02.pdf http://www.informatik.uni-freiburg.de/~neubauer/papers/icfp02.ps.gz -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig Haskell: lazy, yet functional. http://haskell.org/ Aqsis: RenderMan for free. http://aqsis.com/