Opened 3 years ago
Last modified 4 weeks ago
#11350 new feature request
Allow visible type application in patterns
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.1 |
Keywords: | TypeApplications PatternSynonyms | Cc: | adamgundry, RyanGlScott, jeltsch, vagarenko, jpbernardy |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #11385, #13159, #13158 | Differential Rev(s): | |
Wiki Page: |
Description
Constructors (and pattern synonyms) when treated as expressions may be applied to types:
{-# LANGUAGE TypeApplications #-} Nothing :: Maybe a Nothing @() :: Maybe () pattern Pair :: a -> a -> (a, a) pattern Pair x y = (x, y) Pair :: a -> a -> (a, a) Pair @Int :: Int -> Int -> (Int, Int)
But using them in patterns won't parse:
-- parse error in pattern: @Int maybeToList :: Maybe Int -> [Int] maybeToList (Nothing @Int) = [] maybeToList (Just @Int x) = [x] -- parse error in pattern: @Int add :: (Int, Int) -> Int add (Pair @Int x y) = x + y
Change History (23)
comment:1 follow-up: 2 Changed 3 years ago by
comment:2 Changed 3 years ago by
This should make the code in Richard's comment compile:
headOfList :: forall a. [a] -> Maybe a headOfList (Nil @[] @a) = Nothing @a headOfList (Cons @[] @a x _) = Just x
The rest of his comment applies to, this is not for dynamically branching on types although that could certainly be added as a feature!
doubleWhenInt :: forall a. Typeable a => a -> a doubleWhenInt a = case eqT @Int @a of Just Refl -> a + a Nothing -> a -- Becomes… doubleWhenInt :: forall a. Typeable a => a -> a doubleWhenInt @Int n = n + n doubleWhenInt @_ a = a
comment:3 Changed 3 years ago by
Cc: | adamgundry added |
---|
Yes, this is a good idea. It would give a much nicer way to bind (particularly existential) type variables than the current ScopedTypeVariables
hack. I think typecase should be treated separately though, and with lower priority (cf. #11387).
comment:4 Changed 3 years ago by
While commenting on #11441, what about lambdas?
-- Should work, given proposal. id :: forall a. a -> a id @a x = x -- Also. id :: forall a. a -> a id (@ a) (x :: a) = x -- What about this? id :: forall a. a -> a id = \ (@ a) (x :: a) -> x -- Or this id :: b -> b id = \ (@ a) (x :: a) -> x
Same question extends to LambdaCase
.
comment:5 Changed 3 years ago by
Yes. I think all of these should work, modulo parsing. (I'm worried about (@ a)
instead of @a
. Would need to test to be sure.)
comment:6 Changed 2 years ago by
Cc: | RyanGlScott added |
---|
comment:7 Changed 2 years ago by
See comment:1:ticket:11638 for some detailed thoughts about design challenges here.
comment:8 Changed 2 years ago by
Notes, similar to GHC.OverloadedLabels.IsLabel:
class IsLeibel (str::Symbol) a where fromLeibel :: a
would the following work
instance forall x r a. HasField x r a => IsLeibel x (r -> a) where fromLeibel :: r -> a fromLeibel @x = getField @x
Does fromLeibel @x
bring x
into scope, shadowing instance forall x r a.
?
comment:9 Changed 2 years ago by
That's a great question. It would have to be addressed in the design. I lean toward "no", because this seems useless other than for renaming.
comment:11 Changed 2 years ago by
Use case: with newListArray
newListArray :: (MArray a e m, Ix i) => (i, i) -> [e] -> m (a i e)
we want to pick an instance of MArray
many of whom have this form
instance MArray (STUArray s) Word (ST s) instance MArray (STUArray s) Int (ST s) instance MArray (STUArray s) Float (ST s) instance MArray (STUArray s) Bool (ST s)
so you try
newListArray @(STArray _s1) @Bool @(ST _s2) @Int :: MArray (STArray t) Bool (ST t1) => (Int, Int) -> [Bool] -> ST t1 (STArray t Int Bool)
but we need to unify _s1
and _s2
if we want to discharge the constraint, using syntax from ticket:11385#comment:2
\ @s -> newListArray @(STArray s) @Bool @(ST s) @Int
the alternative being newListArray @(STArray s) @Bool @(ST s) @Int :: forall s. _
(which isn't that bad because there are no additional constraints: if we had left @Int
off it would not work and we would have to write
newListArray @(STArray s) @Bool @(ST s) :: forall s i. Ix i => (i, i) -> _
instead)
comment:12 Changed 2 years ago by
Have only referenced this in passing: Allow type application for methods
class Semigroup a where (<>) @a :: a -> a -> a class Semigroup a => Monoid a where mempty @a :: a
and their instances with some #12363
instance (Semigroup a, Semigroup b) => Semigroup (a, b) where (<>) @(a, b) :: (a, b) -> (a, b) -> (a, b) (a1, b1) <> @(a, b) (a2, b2) = (a1 <> @a a2, b1 <> @b b2) instance (Monoid a, Monoid b) => Monoid (a, b) where mempty @(a, b) :: (a, b) mempty @(a, b) = (mempty @a, mempty @b) instance Semigroup b => Semigroup (a -> b) where (<>) @(a -> b) :: (a -> b) -> (a -> b) -> (a -> b) (f <> @(a -> b) g) x = f x <> @b g x -- ^ not recommended style class Monoid b => Monoid (a -> b) where mempty @(a -> b) :: a -> b mempty @(a -> b) _ = mempty @b
The type variables should probably match the order of application a regular expression context.
comment:13 Changed 2 years ago by
dynHead :: Dynamic -> Maybe Dynamic dynHead (Dyn (rxs :: TypeRep txs) (xs :: txs)) = do App rl rx <- splitApp rxs Refl <- rl `eqT` (typeRep :: TypeRep []) return (Dyn rx (head xs))
can be written as (I'm not sure about the Con
definition)
pattern (:<->:) :: () => fa ~ f a => TypeRep f -> TypeRep a -> TypeRep fa pattern f :<->: a <- (splitApp -> Just (App f a)) where f :<->: a = TypeApp f a pattern Con :: forall (u :: k1) (b :: k2). TypeRep u => u ~~ b => TypeRep b pattern Con <- (eqT (typeRep @k1 @u) -> Just HRefl) where Con = typeRep @k1 @u pattern :: () => [Int] ~~ t => TypeRep t pattern ListInt = Con @_ @[] :<->: Con @_ @Int dynHead :: Dynamic -> Maybe Dynamic dynHead (Dyn (Con @_ @[] :<->: a) (x:_)) = Just (Dyn a x) dynHeadInt :: Dynamic -> Maybe Dynamic dynHeadInt (Dyn ListInt (x:_)) = Just (Dyn (Con @_ @Int) x)
that should work the same as
pattern Int :: () => Int ~~ int => T int pattern Int <- (eqT (ty @Type @Int) -> Just HRefl) where Int = typeRep pattern List :: () => [] ~~ list => T list pattern List <- (eqT (ty @(Type -> Type) @[]) -> Just HRefl) where List = typeRep pattern :: () => [Int] ~~ t => TypeRep t pattern ListInt = List :<->: Int
Should also be able to be defined (?)
pattern Int :: () => Int ~~ int => T int pattern Int = Con @Type @Int pattern List :: () => [] ~~ list => T list pattern List = Con @(Type -> Type) @[]
Edit: If we want to get the type of flip
as applied to id
, we would have done
infixl 0 `asAppliedTo` asAppliedTo :: (a -> b) -> a -> (a -> b) asAppliedTo f _ = f flip `asAppliedTo` id :: ((a -> b) -> (a -> b)) -> (a -> (a -> b) -> b)
with the advent of type applications we can write
(flip @(a -> b) @a @b :: forall a b. _) :: ((a -> b) -> (a -> b)) -> (a -> (a -> b) -> b)
With this ticket
(\@a @b -> flip @(a -> b) @a @b) :: ((a -> b) -> (a -> b)) -> (a -> (a -> b) -> b)
Edit 2: This should work:
uncheck1 :: forall a. (forall b. (a -> b) -> b) -> a uncheck1 @a ℓ = ℓ @a (id @a) check1 :: forall a. a -> (forall b. (a -> b) -> b) check1 @a x @b f = fx where fx :: b fx = f x
Currently non-prenex type variables don't scope over the function (this was discussed in another ticket) but we could do it with this.
comment:14 Changed 20 months ago by
Related Tickets: | #11385 → #11385, #13159 |
---|
#13159 discusses this idea w.r.t. pattern synonyms.
comment:15 Changed 20 months ago by
Related Tickets: | #11385, #13159 → #11385, #13159, #13158 |
---|
comment:16 Changed 19 months ago by
#13430 points to a case from Stack Overflow where this was needed in the wild.
comment:17 Changed 18 months ago by
Using the types from Glambda, can we use this to implement
refineTy_ :: Ty -> (forall ty. ITy ty => Proxy ty -> r) -> r refineTy_ IntTy k = k @Int Proxy refineTy_ BoolTy k = k @Bool Proxy refineTy_ (Arr a b) k = refineTy a $ \(Proxy :: Proxy a_ty) -> refineTy b $ \(Proxy :: Proxy b_ty) -> k (Proxy :: Proxy (a_ty -> b_ty))
without Proxy ty
?
refineTy_ :: Ty -> (forall ty. ITy ty => r) -> r refineTy_ IntTy k = k @Int refineTy_ BoolTy k = k @Bool refineTy_ (Arr a b) k = refineTy a $ \@a_ty -> refineTy b $ \@b_ty -> k @(a_ty -> b_ty)
comment:18 Changed 13 months ago by
Cc: | jeltsch added |
---|
Visible type application in patterns would be extremely useful for implementing core transformations in the new version of the incremental-computing
package.
comment:19 Changed 13 months ago by
Visible type application in patterns would be extremely useful for implementing core transformations in the new version of the incremental-computing package.
Could you distil some motivating examples from your package? It's good to know it'd be useful, but better to be able to see the usefulness. Thanks!
comment:20 Changed 12 months ago by
Cc: | vagarenko added |
---|
comment:21 Changed 3 months ago by
comment:22 Changed 6 weeks ago by
Cc: | jpbernardy added |
---|
Relevant note on ⟦Lexing type applications⟧