#11385 closed feature request (duplicate)

Unify named wildcards in different type applications

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.1
Keywords: NamedWildCards TypeApplications Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #11350 Differential Rev(s):
Wiki Page:

Description

(motivating post)

I would like to use type application to specialize

Sub :: forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub @(Ord _a) @(Eq _a) :: forall {a}. (Ord a => Dict (Eq a)) -> Ord a :- Eq a

and

map :: forall a b. (a -> b) -> [a] -> [b]
map @_a @_a :: forall {a}. (a -> a) -> [a] -> [a]

Is there a fundamental reason why named wildcards are not allowed to unify between type applications within the same expression? Documentation:

These are called named wildcards. All occurrences of the same named wildcard within one type signature will unify to the same type.

I don't know if this is intended.

Change History (10)

comment:1 Changed 17 months ago by Iceland_jack

-- asTypeOf :: a -> a -> a
asTypeOf = const @_a @_a

comment:2 Changed 17 months ago by goldfire

Just seeing this now (missed it the first time it went through my inbox).

I'm uncertain about this one. The current behavior is in line with the documentation, in that both arguments to, e.g., const are different types. So I think it's behaving according to spec.

Should the spec change? Perhaps. If I recall correctly, there was a long and tortuous debate about the scoping of named wildcards, with all sides having good arguments in their favor. The nice thing about the current rule is that it's exceedingly simple and easy to predict. With your proposed rule, then you could write f @_a (<something long>) @_a and have the two _as share a scope. So I think I've convinced myself to lean against this idea, but I'm open to argument.

A better solution is to allow visible type abstraction:

asTypeOf = \ @a -> const @a @a

That way, you can say exactly what you mean.

comment:3 in reply to:  2 Changed 17 months ago by Iceland_jack

I disliked the lack of binders in my idea. That would be fixed by

Replying to goldfire:

asTypeOf = \ @a -> const @a @a

like comment:4:ticket:11350 and comment:1:ticket:11638. Let me see if I understand:

add4 :: (Enum a, Enum b) => a -> b -> Int
add4 a b = (fromEnum a + fromEnum b) `mod` 4

if you want add4 :: Enum a => a -> a -> Int you write

-- add4 @_a @_a`

\ @a -> add4 @a @a 
  :: Enum a => a -> a -> Int
-- Sub @(Ord _a) @(Eq _a)

\ @a -> Sub @(Ord a) @(Eq a) 
  :: (Ord a => Dict (Eq a)) -> Ord a :- Eq a
-- map @_a @_a

\ @a -> map @a @a 
  :: (a -> a) -> [a] -> [a]

LGTM.


It may be worth allowing

(\ @a -> map @a @a) @Int
  :: (Int -> Int) -> [Int] -> [Int]

comment:4 Changed 17 months ago by Iceland_jack

Continuing with ticket comment:4:ticket:11350, these make sense to me

asTypeOf @a = const @a @a

endomap @a = fmap @[] @a @a

but wait, asTypeOf @a × endomap @a bind a new type variable. How does that mesh with your intuition from comment:9:ticket:11350?

asTypeOf = \ @a -> const @a @a

-- vs

asTypeOf @a = const @a @a

-- vs

asTypeOf :: forall a. a -> a -> a
asTypeOf @a = const @a @a

-- vs

asTypeOf :: forall a. a -> a -> a
asTypeOf @b = const @b @b
Last edited 17 months ago by Iceland_jack (previous) (diff)

comment:5 Changed 17 months ago by goldfire

I'm assuming your :: ... in comment:3 are meant to be inferred, not part of what the user writes. Then yes. And your final example in comment:3 should most certainly be allowed; if it's not, we've designed the thing very wrongly.

And I agree with all your examples in comment:4 except, possibly, the last. But it's probably just simpler to accept the last example along with the others.

How does this contrast with comment:9:ticket:11350? These are top-level, whereas those are in an instance declaration. I think it's reasonable to have slightly different behavior. In both cases, the function body is interpreted with respect to the user-written type signature for the function. It's just that, in the instance case, the user-written type signature isn't really the full story. But I think it's all OK.

comment:6 in reply to:  5 Changed 17 months ago by Iceland_jack

Replying to goldfire:

I'm assuming your :: ... in comment:3 are meant to be inferred, not part of what the user writes.

Yes

Replying to goldfire:

Then yes. And your final example in comment:3 should most certainly be allowed; ...

And I agree with all your examples in comment:4 except, possibly, the last. But it's probably just simpler to accept the last example along with the others.

... But I think it's all OK.

Great!

comment:7 Changed 16 months ago by Iceland_jack

Trying to wrap the reflection API without Proxy, is there a way to implement this without visible type abstraction? This is reflect and reify

reflect_ :: forall (s :: *) a. Reifies s a => a
reflect_ = reflect @s Proxy

reify_ :: a -> (forall (s :: *). Reifies s a => r) -> r
reify_ a f = reify a (\(Proxy :: Proxy s) -> f @s)

Would this allow

reify 10 $ \p -> reflect p + reflect p

to be written as ?

reify_ 10 $ \ @p -> reflect_ @p + reflect_ @p

Minimal reflection API:

{-# Language RankNTypes, TypeApplications, KindSignatures, MultiParamTypeClasses, FunctionalDependencies, ScopedTypeVariables, AllowAmbiguousTypes #-}

import Unsafe.Coerce

data Proxy k = Proxy

class Reifies s a | s -> a where
  reflect :: proxy s -> a

newtype Magic a r = Magic (forall (s :: *). Reifies s a => Proxy s -> r)

reify :: forall a r. a -> (forall (s :: *). Reifies s a => Proxy s -> r) -> r
reify a k = unsafeCoerce (Magic k :: Magic a r) (const a) Proxy
{-# INLINE reify #-}
Last edited 16 months ago by Iceland_jack (previous) (diff)

comment:8 Changed 16 months ago by Iceland_jack

comment:9 in reply to:  7 Changed 16 months ago by goldfire

Your reify_ in comment:7 certainly seems plausible. I would expect that to work with visible type abstraction.

Is there any difference now between this ticket and #11350? It seems not. Perhaps we should merge.

comment:10 Changed 15 months ago by simonpj

Resolution: duplicate
Status: newclosed

OK well I'll close this one them, in favour of #11350

Note: See TracTickets for help on using tickets.