Type operators in GHC

[Edward Kmett]

Iavor: Wow, I really like the >--c--> trick at the type level.

Note: we can shorten that somewhat and improve the fixity to associate
correctly, matching the associativity of (->), which fortunately associates
to the right. (associating to the left can be done with a similar trick,
based on the original version of this hack by Chung-Chieh Shan.)

{-# LANGUAGE TypeOperators, PolyKinds #-}
import Control.Category

infixr 0 >~
infixr 0 ~>

type (>~) a b = b a
type (~>) a b = a b

g :: Category c => (x >~c~> y) -> (y >~c~> z) -> x >~c~> z
g = undefined

Note, this also has the benefit of picking the correct associativity for
>~c~>. Unlike naively using a locally bound (~>) and avoids the headaches
of picking (-->) and (--->) or something equally hideous when working with
two categories.

class (Category c, Category d) => CFunctor f c d | f c -> d, f d -> c where
  cmap :: (a >~c~> b) -> f a >~d~> f b

-Edward

On Mon, Sep 17, 2012 at 1:02 PM, Sjoerd Visscher <sjoerd at w3future.com>wrote:

> Hi,
>
> Note that nobody was suggesting two pragmas with incompatible behaviors,
> only to have just one symbol reserved to still be able to have type
> operator variables.
>
> I do like your suggestion, although >--c--> is quite a bit longer than ~>.
>
> Sjoerd
>
> On Sep 17, 2012, at 6:28 PM, Iavor Diatchki wrote:
>
> Hello,
>
> I think that it would be a mistake to have two pragmas with incompatible
> behaviors:  for example, we would not be able to write modules that use
> Conal's libraries and, say, the type nats I've been working on.
> If the main issue is the notation for arrows, has anoyone played with what
> can be done with the current (7.6) system?  I just thought of two
> variations that seem to provide a decent notation for writing arrow-ish
> programs.  The second one, in particular, mirrors the arrow notation at the
> value level, so perhaps that would be enough?
>
> -Iavor
>
>
> {-# LANGUAGE TypeOperators, KindSignatures #-}
> module Test where
>
> import Control.Category
>
> -- Variant 1: Post-fix annotation
>
> type (a ---> b) c = c a b
>
> f :: Category c => (x ---> y) c -> (y ---> z) c -> (x ---> z) c
> f = undefined
>
>
> -- Variant 2: Arrow notation
>
> type a >-- (c :: * -> * -> *) = c a
> type c --> b                  = c b
>
> infix 2 >--
> infix 1 -->
>
> g :: Category c => (x >--c--> y) -> (y >--c--> z) -> (x >--c--> z)
> g = undefined
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120917/9694eb50/attachment-0001.htm>