Opened 18 months ago
Last modified 2 months 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 |
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 (17)
comment:1 follow-up: 2 Changed 18 months ago by
comment:2 Changed 18 months 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 18 months 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 17 months 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 17 months 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 13 months ago by
Cc: | RyanGlScott added |
---|
comment:7 Changed 13 months ago by
See comment:1:ticket:11638 for some detailed thoughts about design challenges here.
comment:8 Changed 12 months 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 12 months 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 9 months 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 9 months 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 8 months 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 5 months ago by
Related Tickets: | #11385 → #11385, #13159 |
---|
#13159 discusses this idea w.r.t. pattern synonyms.
comment:15 Changed 5 months ago by
Related Tickets: | #11385, #13159 → #11385, #13159, #13158 |
---|
comment:16 Changed 3 months ago by
#13430 points to a case from Stack Overflow where this was needed in the wild.
comment:17 Changed 2 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 a $ \(Proxy :: Proxy b_ty) -> k @(a_ty -> b_ty) Proxy
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 a $ \@b_ty -> k @(a_ty -> b_ty)
Relevant note on ⟦Lexing type applications⟧