[Haskell-cafe] Partially-applied type synonyms?
ccshan at post.harvard.edu
Tue Aug 31 13:00:44 EDT 2004
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.
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.
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/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Size: 189 bytes
Desc: Digital signature
Url : http://www.haskell.org//pipermail/haskell-cafe/attachments/20040831/107138f8/attachment.bin
More information about the Haskell-Cafe