#12363: Type application for infix -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: lowest | Milestone: Component: Compiler | Version: 8.0.1 (Parser) | Keywords: Resolution: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Just passing by ---- A [http://sf.snu.ac.kr/jeehoon.kang/assets/bs_math.pdf definition] of composition of an opposite category. The different instantiations of composition are made explicit but the arrows are cast implicitly: {{{ f ∘_C^op g = g ∘_C f }}} Awodey uses the notation `f* : B* -> A*` in `ℂ^op` for `f : A -> B` in `ℂ` making conversions between categories explicit. The category of the identity arrow is named but not of composition: {{{ 1_ℂ* = (1_ℂ)* f* ∘ g* = (g ∘ f)* }}} Haskell makes switching between categories explicit, using `Op f :: (Op ℂ) B A` for `f :: ℂ A B` {{{#!hs type Cat k = k -> k -> Type newtype Op :: Cat i -> Cat i where Op :: cat b a -> (Op cat) a b instance Category cat => Category (Op cat) where id :: (Op cat) a a id = Op id (.) :: (Op cat) b c -> (Op cat) a b -> (Op cat) a c Op f . Op g = Op (g . f) }}} can be made more explicit by {{{#!hs id :: (Op cat) a a id = Op (id @cat) (.) :: (Op cat) b c -> (Op cat) a b -> (Op cat) a c Op f . Op g = Op (g . @cat f) }}} ---- A separate proposal is visible type applications on methods, corresponding to their instance type arguments (`Op cat` in this case) which gives us an (overly?) explicit definition {{{#!hs id @(Op cat) = Op (id @cat) Op f . @(Op cat) Op g = Op (g . @cat f) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler