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@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@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users