Opened 22 months ago

Last modified 6 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, jeltsch, vagarenko
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 (20)

comment:1 Changed 22 months ago by Iceland_jack

comment:2 in reply to:  1 Changed 22 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 22 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 21 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 21 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 17 months ago by RyanGlScott

Cc: RyanGlScott added

comment:7 Changed 17 months ago by goldfire

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

comment:8 Changed 16 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 16 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 15 months ago by Iceland_jack

An additional comment on

comment:11 Changed 13 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 13 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 12 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 12 months ago by Iceland_jack (previous) (diff)

comment:14 Changed 9 months ago by goldfire

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

comment:15 Changed 8 months ago by simonpj

comment:16 Changed 7 months ago by simonpj

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

comment:17 Changed 6 months 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 b $ \(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 b $ \@b_ty -> 
    k @(a_ty -> b_ty)
Last edited 5 weeks ago by Iceland_jack (previous) (diff)

comment:18 Changed 5 weeks ago by jeltsch

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 5 weeks ago by simonpj

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 6 days ago by vagarenko

Cc: vagarenko added
Note: See TracTickets for help on using tickets.