Opened 16 months ago

Last modified 12 days 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 Changed 16 months ago by Iceland_jack

comment:2 in reply to:  1 Changed 16 months ago by Iceland_jack

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 16 months ago by adamgundry

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 15 months ago by Iceland_jack

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 15 months ago by goldfire

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 11 months ago by RyanGlScott

Cc: RyanGlScott added

comment:7 Changed 11 months ago by goldfire

See comment:1:ticket:11638 for some detailed thoughts about design challenges here.

comment:8 Changed 10 months ago by Iceland_jack

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 10 months ago by goldfire

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:10 Changed 9 months ago by Iceland_jack

An additional comment on

comment:11 Changed 7 months ago by Iceland_jack

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 7 months ago by Iceland_jack

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 7 months ago by Iceland_jack

comment

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.

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

comment:14 Changed 3 months ago by goldfire

#13159 discusses this idea w.r.t. pattern synonyms.

comment:15 Changed 3 months ago by simonpj

comment:16 Changed 6 weeks ago by simonpj

#13430 points to a case from Stack Overflow where this was needed in the wild.

comment:17 Changed 12 days ago by Iceland_jack

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)
Note: See TracTickets for help on using tickets.