Opened 15 months ago
Last modified 3 months 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 (23)
comment:1 follow-up: 3 Changed 15 months ago by
comment:2 Changed 15 months ago by
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 Changed 15 months ago by
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 15 months ago by
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
comment:5 Changed 14 months ago by
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) -- AssociativitySimilarly, 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 gThis is the "composition law".
Rule #2:
map
must transform the identity in the source category to the identity in the destination category:map idA = idBThis 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
comment:6 Changed 13 months ago by
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
comment:7 Changed 13 months ago by
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 follow-up: 9 Changed 13 months ago by
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 Changed 13 months ago by
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 13 months ago by
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
..
comment:11 Changed 13 months ago by
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 12 months ago by
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 oflift
: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.
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)
comment:13 Changed 9 months ago by
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 9 months ago by
With #13097
>>> 10 < 20 True >>> 10 < @(Down _) 20 False >>> 10 < @(Down (Down _)) 20 True
>>> 10 < @Down{} 20 False >>> 10 < @(Down Down{}) 20 True
comment:15 follow-ups: 16 17 Changed 9 months ago by
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 Changed 9 months ago by
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 Changed 9 months ago by
comment:18 follow-up: 19 Changed 8 months ago by
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 Changed 8 months ago by
Replying to rwbarton:
I know the manual says you can write things like
f x @Bool
meaning(f x) @Bool
iff
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:21 Changed 6 months ago by
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 3 months ago by
Cc: | RyanGlScott added |
---|
comment:23 Changed 3 months ago by
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.
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.