Opened 17 months ago

Last modified 9 days ago

#12363 new feature request

Type application for infix

Reported by: Iceland_jack Owned by:
Priority: lowest Milestone:
Component: Compiler (Parser) Version: 8.0.1
Keywords: TypeApplications Cc: RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

1 + @Int 10 is a parse error, I would like it to mean the same as

(+) @Int 1 10

Thoughts?


Also

>>> pure `foldMap` @Maybe @[_] Just 'a'
"a"

>>> foldMap @Maybe @[_] pure (Just 'a')
"a"

Change History (25)

comment:1 Changed 17 months ago 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.

comment:2 Changed 17 months ago by Iceland_jack

In my current code I need to give a type hint to an assignment

ptr := @elt value

Amazingly this can be emulated with some trickery

-- infixl 0 ◃, <|, ▹, |>
-- (◃)  = flip ($)
-- (<|) = flip ($)
-- (▹)  = ($)
-- (|>) = ($)
ptr <|(:=) @elt|> value

but at that point this is clearer

assign @elt ptr value

comment:3 in reply to:  1 Changed 17 months ago by Iceland_jack

Replying to 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:

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?

instance Eq a => Eq [a] where
  ...
  (x:xs) == (y:ys) = x == @a y && xs == @[a] ys

I'm no fan of the foldMap example.

comment:4 Changed 17 months ago by Iceland_jack

It's reminiscent of math notation, for example homomorphisms:

instance Semigroup Int where
  (<>) = (+)
-- |abc| ◇_ℕ |xyz| = |abc ◇_Σ⁺ xyz|

length ('a':|"bc") <> @Int length ('x':|"yz")
--   ==
length (('a':|"bc") <> @(NonEmpty Char) ('x':|"yz"))

where it is clear that the two <> are very different functions.


We can already achieve the “mathematical notation” for the identity element:

instance Monoid Int where
  mempty  = 0
  mappend = (+) 
-- |ε_Σ*| = ε_ℕ

length (mempty @String)
--   ==
mempty @Int
Last edited 17 months ago by Iceland_jack (previous) (diff)

comment:5 Changed 16 months ago by Iceland_jack

This is interesting. Usually Haddock displays

((~) * a b, Data a) => Data ((:~:) * a b)

This could be

(a ~ @* b, Data a) => Data (q :~: @* b)

The asymmetry is awkward but I prefer it to the current version. It could of course be written

((~) @* a b, Data a) => Data ((:~:) @* a b)

using #12045 it would be valid code.


Edit

Considering the Semigroup / Monoid instances for WriteAction (How to Twist Pointers without Breaking Them)

newtype WriteAction = WA (Pointer -> IO ()) deriving (Semigroup, Monoid)

you can write this for Monoid's mempty

  mempty @WriteAction
= WA $ mempty @(Pointer -> IO ())
= WA $ \_ -> mempty @(IO ())
= WA $ \_ -> pure (mempty @())
= WA $ \_ -> pure ()
= WA $ \_ -> [| () |]

and this for Semigroup's <>

  WA a <> @WriteAction WA b 
= WA $ a <> @(Pointer -> IO ()) b
= WA $ \ptr -> a ptr <> @(IO ()) b ptr
= WA $ \ptr -> liftA2 (mappend @()) (a ptr) (b ptr)
= WA $ \ptr -> [| a ptr <> @() b ptr |]

This shows the different instantiations of <> but I admit this is starting to look confusing :)


Edit 2: Gabriel's post on The functor design pattern

I will notationally distinguish between the two categories in question so I can be crystal clear about the mathematical definition of a functor. I will denote our "source" category's identity as idA and its composition as (._A), and these must obey the category laws:

-- Yes, "._A" is ugly, I know
idA ._A f = f                      -- Left identity

f ._A id = f                       -- Right identity

(f ._A g) ._A h = f ._A (g ._A h)  -- Associativity

Similarly, I denote the "destination" category's identity as idB and its composition as (._B), which also must obey the category laws:

idB ._B f = f                      -- Left identity

f ._B idB = f                      -- Right identity

(f ._B g) ._B h = f ._B (g ._B h)  -- Associativity

[…]

Rule #1: map must transform the composition operator in the source category to the composition operator in the destination category:

map (f ._A g) = map f ._B map g

This is the "composition law".

Rule #2: map must transform the identity in the source category to the identity in the destination category:

map idA = idB

This is the "identity law".

Given

import Prelude hiding ((.), id)
import Control.Category
import Data.Kind

type Cat i = i -> i -> Type

data A :: Cat i
data B :: Cat i

instance Category A
instance Category B

this would be valid syntax

id @A . @A f = f
id @B . @B f = f

f . @A id @A = f
f . @B id @B = f

(f . @A g) . @A h = f . @A (g . @A h)
(f . @B g) . @B h = f . @B (g . @B h)

map (id @A)    = id @B
map (f . @A g) = map f . @B map g
Last edited 15 months ago by Iceland_jack (previous) (diff)

comment:6 Changed 15 months ago by Iceland_jack

a `asTypeIn` f = a where _ = f a

Checking the type of fails due to ambiguous Functor, Applicative constraints

flip id `asTypeIn` \x -> x <$> undefined <*> undefined <*> undefined

The user must possess prior knowledge and rewrite the expression

-- 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

flip id `asTypeIn` \x -> x <$> @[] undefined <*> undefined <*> undefined

flip id `asTypeIn` \x -> x <$> @[] undefined <*> @[] undefined <*> @[] undefined
Last edited 15 months ago by Iceland_jack (previous) (diff)

comment:7 Changed 15 months ago by Iceland_jack

Just passing by


A 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

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

  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

id @(Op cat) = Op (id @cat)

Op f . @(Op cat) Op g = Op (g . @cat f)

comment:8 Changed 15 months ago 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.

comment:9 in reply to:  8 Changed 15 months ago by Iceland_jack

Replying to 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.

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
    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
    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)

comment:10 Changed 15 months ago by Iceland_jack

The code from #12507, whether or not it's supposed to compile, it would be nice to be able to specify the result type r

(?) :: forall r fields. Rec fields -> (fields => r) -> r
Rec ? e = e 
access = record ? ?a

Doesn't compile, but this does

-- access :: (?a::Int) => Int
access = (?) @Int record ?a

could be written as record ? @Int ?a..

Last edited 15 months ago by Iceland_jack (previous) (diff)

comment:11 Changed 15 months ago by Iceland_jack

An extended version of the Eq example,

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

comment:12 Changed 14 months ago 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.

Monad Transformers and Modular Interpreters

This effectively uses a different formulation of MonadTrans with a Monad constraint on t m (see this)

class (Monad m, Monad (t m)) => MonadT t m where
  lift :: m a -> (t m) a

It preserves pure if these functions are equal

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:

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 infixiaticating it

bind1 k m = lift ((>>=) @m m k)
bind2 k m = (>>=) @(t m) (lift m) (lift . k)

We can of course be even more explicit

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

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:

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)
Last edited 14 months ago by Iceland_jack (previous) (diff)

comment:13 Changed 11 months ago by Iceland_jack

Fits well with catch, catchIO, catchSTM idiom

-- 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

-- 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 Control Flow in Haskell (3) - Flow with Variant

-- 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"

comment:14 Changed 10 months ago by Iceland_jack

With #13097

>>> 10 < 20 
True

>>> 10 < @(Down _) 20
False

>>> 10 < @(Down (Down _)) 20
True

With #13097 + #12465

>>> 10 < @Down{} 20
False

>>> 10 < @(Down Down{}) 20
True
Last edited 10 months ago by Iceland_jack (previous) (diff)

comment:15 Changed 10 months ago 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.

comment:16 in reply to:  15 Changed 10 months ago by Iceland_jack

Replying to 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.

Just According to Keikaku.⁽¹⁾

⁽¹⁾ (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 intervals package documentation gives a lot of good examples where this is useful:

-- >>> (5 ... 10 :: Interval Double) <! (20 ... 30 :: Interval Double)
-- True
>>> (5 ... 0) <! @Double (20 ... 30)
True

-- >>> (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

-- >>> (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

-- n `hashWithSalt` (fromIntegral (ptrToIntPtr s) :: Int)
-- n `hashWithSalt` fromIntegral @_ @Int (ptrToIntPtr s)
n `hashWithSalt` @Int fromIntegral (ptrToIntPtr s)
-- 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

-- 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 this

  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 ==

  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

comment:17 in reply to:  15 Changed 10 months ago by goldfire

Replying to 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.

Yes, to my chagrin, I agree here. I retract my -1 from comment:1.

comment:18 Changed 10 months ago 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.

comment:19 in reply to:  18 Changed 10 months ago by goldfire

Replying to 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:

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.

comment:20 Changed 9 months ago by Iceland_jack

I'll add thoughts and examples to this gist

comment:21 Changed 8 months ago by vagarenko

I tried to write

a `foo` @Bar b

the other day and was surprised it didn't work.

I'd like to see this implemented.

comment:22 Changed 5 months ago by RyanGlScott

Cc: RyanGlScott added

comment:23 Changed 4 months ago 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.

comment:24 Changed 9 days ago 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

comment:25 Changed 9 days ago 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.

Note: See TracTickets for help on using tickets.