[Haskell-cafe] Partially-applied type synonyms?

[Chung-chieh Shan]

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/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://www.haskell.org//pipermail/haskell-cafe/attachments/20040831/107138f8/attachment.bin