[GHC] #12363: Type application for infix

#12363: Type application for infix -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature | Status: new request | Priority: lowest | Milestone: Component: Compiler | Version: 8.0.1 (Parser) | Keywords: | Operating System: Unknown/Multiple TypeApplications | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- `1 + @Int 10` is a parse error, I would like it to mean the same as {{{#!hs (+) @Int 1 10 }}} Thoughts? ---- Also {{{#!hs
pure `foldMap` @Maybe @[_] Just 'a' "a"
foldMap @Maybe @[_] pure (Just 'a') "a" }}}
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 goldfire): I suppose this capitalizes on the fact that things beginning with `@` can't be functions that take further parameters. But I find this quite difficult to understand, with `@`-arguments binding tighter than other arguments. -1 from me, sorry. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): In my current code I need to give a type hint to an assignment {{{#!hs ptr := @elt value }}} Amazingly this can be emulated with some trickery {{{#!hs -- infixl 0 ◃, <|, ▹, |> -- (◃) = flip ($) -- (<|) = flip ($) -- (▹) = ($) -- (|>) = ($) ptr <|(:=) @elt|> value }}} but at that point this is clearer {{{#!hs assign @elt ptr value }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): Replying to [comment:1 goldfire]:
-1 from me, sorry.
I understand your -1. I will write examples that come to mind without pushing my point. I feel this has pedagogic value: {{{#!hs instance Eq a => Eq [a] where (==) :: [a] -> [a] -> Bool [] == [] = True (x:xs) == (y:ys) = x == y && xs == ys _ == _ = False }}} in the second equation `==` is called at two different types, wouldn't this be a beautiful way of showing that? {{{#!hs instance Eq a => Eq [a] where ... (x:xs) == (y:ys) = x == @a y && xs == @[a] ys }}} I'm no fan of the `foldMap` example. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): It's reminiscent of math notation, for example homomorphisms: {{{#!hs instance Semigroup Int where (<>) = (+) }}} {{{#!hs -- |abc| ◇_ℕ |xyz| = |abc ◇_Σ∗ xyz| length "abc" <> @Int length "xyz" -- == length ("abc" <> @String "xyz") }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): This is interesting. Usually Haddock displays {{{#!hs ((~) * a b, Data a) => Data ((:~:) * a b) }}} This could be {{{#!hs (a ~ @* b, Data a) => Data (q :~: @* b) }}} The asymmetry is awkward but I prefer it to the current version. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): {{{#!hs a `asTypeIn` f = a where _ = f a }}} Checking the type of fails due to ambiguous `Functor`, `Applicative` constraints {{{#!hs flip id `asTypeIn` \x -> x <$> undefined <*> undefined <*> undefined }}} The user must either possess some prior knowledge and rewrite the expression {{{#!hs -- fixity of <$>, <*> flip id `asTypeIn` \x -> (<$>) @[] x undefined <*> undefined <*> undefined :: a -> (a -> b -> c) -> b -> c -- liftA3 f a b c = f <$> a <*> b <*> c flip id `asTypeIn` \x -> liftA3 @[] x undefined undefined undefined :: a -> (a -> b -> c) -> b -> c -- the return type of `_ <$> _ <*> _ <*> _` is some Applicative `f _` flip id `asTypeIn` \x -> (x <$> undefined <*> undefined <*> undefined :: [_]) :: a -> (a -> b -> c) -> b -> c }}} With infix type application they can directly write {{{#!hs flip id `asTypeIn` \x -> x <$> @[] undefined <*> undefined <*> undefined flip id `asTypeIn` \x -> x <$> @[] undefined <*> @[] undefined <*> @[] undefined }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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 goldfire): These examples are very helpful. Now that you have collected them, I think a good next step is soliciting feedback from the community so that we can see if others agree with you. I'll admit to becoming more convinced by your examples, but I'm still leaning against. Other voices in agreement with yours would make a big difference here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

These examples are very helpful. Now that you have collected them, I
#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): Replying to [comment:8 goldfire]: think a good next step is soliciting feedback from the community so that we can see if others agree with you. I'll admit to becoming more convinced by your examples, but I'm still leaning against. Other voices in agreement with yours would make a big difference here. I agree that this needs input from the community. The notation often feels clunky and asymmetric, mathematicians would use subscript instead. Visual type application (+ partial type signatures) have been very useful * '''Interactive use''' Toying around, getting ''ghci'' to resolve instances for me {{{#!hs mappend @(_ -> _) :: Monoid b => (a -> b) -> (a -> b) -> (a -> b) quickCheck @(_ -> _) :: (Arbitrary a, Show a, Testable b) => (a -> b) -> IO () quickCheck @(Int -> _) :: Testable b => (Int -> b) -> IO () }}} * '''Teaching''' Using valid Haskell syntax to simplify complex signatures that users can verify on their own {{{#!hs length @[] :: [a] -> Int sequence @[] @IO :: [IO a] -> IO [a] }}} Less so in actual code. The same seems true for this so I am not overly concerned with the syntax. Indeed most of the benefits of the examples don't have to do with actual code, rather presenting concepts with explicit/valid syntax or interactive use: allowing users to quickly specify a type without rearranging/rewriting syntax and adding parentheses (`(.) @A (id @A) f`). No need to muck about with expressions which reduces mental load: if you want `<$>` for lists, write `<$> @[]`. If it's all the same I will post examples until told to stop ;) (for operators, `_` with no spaces looks nicer (`1 +_Int 10`) but I won't seriously suggest it) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): The [[https://gist.github.com/llelf/6c01ded225877914f38a code] from #12507, whether or not it's supposed to compile, it would be nice to be able to specify the result type `r` {{{#!hs (?) :: forall r fields. Rec fields -> (fields => r) -> r Rec ? e = e }}} {{{#!hs access = record ? ?a }}} Doesn't compile, but {{{#!hs -- access :: (?a::Int) => Int access = (?) @Int record ?a }}} which could be `record ? @Int ?a`.. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): An extended version of the `Eq` example, {{{#!hs class Eq a where type Logic a (==) :: a -> a -> Logic a instance Eq b => Eq (a -> b) where type Logic (a -> b) = a -> Logic b (==) :: (a -> b) -> (a -> b) -> (a -> Logic b) (f == @(a->b) g) x = f x == @b g x }}} Yuck ugly -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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):
The member function `lift` embeds a computation in monad ''m'' into a monad ''t m''. Furthermore, we expect a monad transformer to ''add'' features, without changing the nature of an existing omputation. We introduce ''Monad Transformer Laws'' to capture the properties of `lift`:
{{{ lift · unit_m = unit_tm
lift (m `bind_m` k) = lift m `bind_tm` (lift · k) }}}
The above laws say that lifting a null computation results in a null computation, and that lifting a sequence of computations is equivalent to first lifting them individually, and then combining them in the lifted monad.
— [http://haskell.cs.yale.edu/wp-content/uploads/2011/02/POPL96-Modular- interpreters.pdf Monad Transformers and Modular Interpreters]
This effectively uses a different formulation of `MonadTrans` with a `Monad` constraint on ''t m'' (see [https://www.reddit.com/r/haskell/comments/50rxci/edward_kmett_monad_homomorp... this]) {{{#!hs class (Monad m, Monad (t m)) => MonadT t m where lift :: m a -> (t m) a }}} It preserves `pure` if these functions are equal {{{#!hs pure1, pure2 :: forall t m a. MonadT t m => a -> (t m) a pure1 = lift . pure @m pure2 = pure @(t m) }}} and with infix type application we can express the preservation of ''bind'' with the following two equations: {{{#!hs bind1, bind2 :: forall t m a b. MonadT t m => (a -> m b) -> (m a -> (t m) b) bind1 k m = lift (m >>= @m k) bind2 k m = lift m >>= @(t m) (lift . k) }}} without awkwardly infixiaticate it {{{#!hs bind1 k m = lift ((>>=) @m m k) bind2 k m = (>>=) @(t m) (lift m) (lift . k) }}} ---- We can of course be even more explicit {{{#!hs bind1, bind2 :: forall t m a b. MonadT t m => (a -> m b) -> (m a -> (t m) b) bind1 k m = lift @t @m @b (m >>= @m @a @b k) bind2 k m = lift @t @m @a m >>= @(t m) @a @b (lift @t @m @b . k) }}} whatevs {{{#!hs lift_ :: forall tm a t m. ((t m ~ tm), MonadT t m) => m a -> t m a lift_ = lift bind1, bind2 :: forall t m a b. Monad_ t m => (a -> m b) -> (m a -> (t m) b) bind1 k m = lift_ @(t m) @b (m >>= @m @a @b k) bind2 k m = lift_ @(t m) @a m >>= @(t m) @a @b (lift_ @(t m) @b . k) }}} ---- Similarly we can write down the laws for other monad morphisms: {{{#!hs foo1, foo2 :: forall m a. MonadIO m => a -> m a foo1 = pure @m foo2 = liftIO . pure @IO bind1, bind2 :: forall m a b. MonadIO m => (a -> IO b) -> (IO a -> m b) bind1 k m = liftIO ((>>=) @IO m k) bind2 k m = (>>=) @m (liftIO m) (liftIO . k) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): Fits well with `catch`, `catchIO`, `catchSTM` idiom {{{#!hs -- do print (a ! 5) `catch` \e -> print (e :: SomeException) -- print (b ! (0,5)) `catch` \e -> print (e :: SomeException) do print (a ! 5) `catch` @SomeException print print (b ! (0,5)) `catch` @SomeException print }}} In that case you could write `print @SomeException` but that will not work if the handler doesn't mention the exception at all {{{#!hs -- rmDir :: FilePath -> IO () -- rmDir dir = removeDirectoryRecursive dir `catch` (const $ return () :: IOException -> IO ()) rmDir :: FilePath -> IO () rmDir dir = removeDirectoryRecursive dir `catch` @IOException const (return ()) }}} (granted `const @_ @IOException` works here, but having a singular place for the type application is nice) and from [http://hsyl20.fr/home/posts/2016-12-12-control-flow-in-haskell- part-3.html Control Flow in Haskell (3) - Flow with Variant] {{{#!hs -- test = f 5 >%~=> (\(a :: A) -> putStrLn "An A has been returned") -- >%~=> (\(b :: B) -> putStrLn "A B has been returned") -- >%~=> (\(c :: C) -> putStrLn "A C has been returned") test = f 5 >%~=> @A \_ -> putStrLn "An A has been returned" >%~=> @B \_ -> putStrLn "A B has been returned" >%~=> @C \_ -> putStrLn "A C has been returned" }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): With #13097 {{{#!hs
10 < 20 True
10 < @(Down _) 20 False
10 < @(Down (Down _)) 20 True }}}
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 rwbarton): I don't know if it's the sheer number of updates to this ticket, but this syntax is starting to look fairly natural to me. Most of these examples don't look like code I would ever write, but the {{{`catch` @IOException}}} example is pretty sweet. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

I don't know if it's the sheer number of updates to this ticket, but
#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): Replying to [comment:15 rwbarton]: this syntax is starting to look fairly natural to me. Just According to Keikaku.⁽¹⁾ ⁽¹⁾ [https://www.reddit.com/r/OutOfTheLoop/comments/467byi/what_the_hell_is_keika... (Translator's note: keikaku means plan)]
Most of these examples don't look like code I would ever write, but the {{{`catch` @IOException}}} example is pretty sweet.
It works especially well with operators where the specified type does not appear in the return type: having to privilege one side over the other feels asymmetric, the [https://hackage.haskell.org/package/intervals intervals] package documentation gives a lot of good examples where this is useful: {{{#!hs -- >>> (5 ... 10 :: Interval Double)
(5 ... 0)
-- >>> (20 ... 40 :: Interval Double) `contains` (15 ... 35 :: Interval Double) -- False
(20 ... 40) `contains` @Double (15 ... 35) False }}}
but also simpler examples, I will avoid writing an explicit annotation if I can {{{#!hs -- >>> (0.1 :: Float) + 0.2 == 0.3 -- True
0.1 + 0.2 == @Float 0.3 True
-- >>> 0.1 + 0.2 == (0.3 :: Double) -- False
0.1 + 0.2 == @Double 0.3 False
-- >>> 0 `elem` [1,2::Int,3] -- False
0 `elem` @[] @Int [1,2,3] False }}}
For most examples you can easily annotate some other part of the expression to get the same effect. My experience is that infix type application leads to less thinking, more consistency (in where the type goes) and more resistance to change: I prefer the uncommented versions {{{#!hs -- n `hashWithSalt` (fromIntegral (ptrToIntPtr s) :: Int) -- n `hashWithSalt` fromIntegral @_ @Int (ptrToIntPtr s) n `hashWithSalt` @Int fromIntegral (ptrToIntPtr s) }}} {{{#!hs -- Var a -> digest c (1 :: Word8) `digest` a -- App f x -> digest c (2 :: Word8) `digest` f `digest` x -- HardType h -> digest c (3 :: Word8) `digest` h -- Forall k tvs cs b -> digest c (4 :: Word8) `digest` k `digest` tvs `digest` cs `digest` b -- Loc _ ty -> digest c ty -- Exists k tvs cs -> digest c (5 :: Word8) `digest` k `digest` tvs `digest` cs -- And xs -> digest c (6 :: Word8) `digest` xs Var a -> c `digest` @Word8 1 `digest` a App f x -> c `digest` @Word8 2 `digest` f `digest` x HardType h -> c `digest` @Word8 3 `digest` h Forall k tvs cs b -> c `digest` @Word8 4 `digest` k `digest` tvs `digest` cs `digest` b Loc _ ty -> c `digest` ty Exists k tvs cs -> c `digest` @Word8 5 `digest` k `digest` tvs `digest` cs And xs -> c `digest` @Word8 6 `digest` xs }}} and {{{#!hs -- tAG_BITS_MAX = (1 `shiftL` tAG_BITS) :: Int tAG_BITS_MAX = 1 `shiftL` @Int tAG_BITS }}} ---- I would still say the main usefulness is pedagogy: I will not introduce invalid syntax when explaining things to newcomers, but for questions like [https://www.reddit.com/r/haskellquestions/comments/5mtk8v/instance_eq_questi... this] {{{#!hs Nodo x ys zs == Nodo x' ys' zs' = x == x' && ys == ys' && zs == zs' }}} maybe it would help to write it like this, to show the different instantiations of `==` {{{#!hs Nodo x ys zs == Nodo x' ys' zs' = x == @a x' && ys == @(Heap a) ys' && zs == @(Heap a) zs' }}} In the end it's up to what the community thinks -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

I don't know if it's the sheer number of updates to this ticket, but
#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 goldfire): Replying to [comment:15 rwbarton]: this syntax is starting to look fairly natural to me. Yes, to my chagrin, I agree here. I retract my -1 from comment:1. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 rwbarton): The fact that type application "telescopes" are normally only applied to single identifiers also helps my brain gloss over the parsing/precedence irregularities here. It's easy enough to read `+ @Int` as a unit. I know the manual says you can write things like `f x @Bool` meaning `(f x) @Bool` if `f` has a suitable type, though I wonder if there are any real uses for that. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 goldfire): Replying to [comment:18 rwbarton]:
I know the manual says you can write things like `f x @Bool` meaning `(f x) @Bool` if `f` has a suitable type, though I wonder if there are any real uses for that.
One plausible-sounding scenario is in specializing a polymorphic function accessed by a record selector: {{{#!hs data Mon'd m = MkMon'd { ret'rn :: forall a. a -> m a } f :: Mon'd m -> ... f dict ... = ... ret'rn dict @Int ... }}} But, yes, frequently the function applied to type parameters is just an identifier. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12363: Type application for infix -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) 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): I'll add thoughts and examples to this [https://gist.github.com/Icelandjack/06bcc4f62cb42ada120839bf409a53e4 gist] -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12363: Type application for infix -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) 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 vagarenko): I tried to write {{{#!hs a `foo` @Bar b }}} the other day and was surprised it didn't work. I'd like to see this implemented. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12363: Type application for infix -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) 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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12363: Type application for infix -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) 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 goldfire): I, for one, am convinced. If someone wants to write a ghc-proposal about this, I'll support it. If no one does, I might on my own someday. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12363: Type application for infix -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) 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 dredozubov): It seems I created a duplicate ticket #14446 I'm linking it to add my two cents to a plethora of examples provided by @Iceland_jack -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:24 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12363: Type application for infix -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) 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 AntC): I'm perturbed by the type argument appearing after the infix operator; whereas with a prefixed function the type argument comes first. In {{{ instance Eq a => Eq [a] where ... (x:xs) == (y:ys) = x == @a y && xs == @[a] ys }}} the prefix form would put `@a` before `x` So my brain has to parse that as `x (== @a) y`. Shouldn't it be like this {{{ (x:xs) == (y:ys) = @a x == y && @[a] xs == ys }}} I notice in @dredozubov's #14446, the `@"foo"` comes before the operator. As to whether the syntax becomes less scary from looking through the examples: no, to me it still looks like perl or Teco. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12363#comment:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC