[GHC] #11385: Unify named wildcards in different type applications
#11385: Unify named wildcards in different type applications -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple NamedWildCards TypeApplications | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- ([https://www.reddit.com/r/haskell/comments/4030lv/unifying_distinct_type_vari... motivating post]) I would like to use type application to specialize {{{#!hs 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 {{{#!hs 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? [https://downloads.haskell.org/~ghc/master/users-guide/glasgow_exts.html #named-wildcards 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11385 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11385: Unify named wildcards in different type applications -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | NamedWildCards TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): {{{#!hs -- asTypeOf :: a -> a -> a asTypeOf = const @_a @_a }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11385#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11385: Unify named wildcards in different type applications -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | NamedWildCards TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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 `_a`s 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11385#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11385: Unify named wildcards in different type applications -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | NamedWildCards TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): I disliked the lack of binders in my idea. That would be fixed by Replying to [comment:2 goldfire]:
{{{ asTypeOf = \ @a -> const @a @a }}}
like comment:4:ticket:11350 and comment:1:ticket:11638. Let me see if I understand: {{{#!hs 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 {{{#!hs -- add4 @_a @_a` \ @a -> add4 @a @a :: Enum a => a -> a -> Int }}} {{{#!hs -- Sub @(Ord _a) @(Eq _a) \ @a -> Sub @(Ord a) @(Eq a) :: (Ord a => Dict (Eq a)) -> Ord a :- Eq a }}} {{{#!hs -- map @_a @_a \ @a -> map @a @a :: (a -> a) -> [a] -> [a] }}} LGTM. ---- It may be worth allowing {{{#!hs (\ @a -> map @a @a) @Int :: (Int -> Int) -> [Int] -> [Int] }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11385#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11385: Unify named wildcards in different type applications -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | NamedWildCards TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Continuing with ticket comment:4:ticket:11350, these make sense to me {{{#!hs 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? {{{#!hs asTypeOf = \ @a -> const @a @a -- vs asTypeOf @a = const @a @a }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11385#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11385: Unify named wildcards in different type applications -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | NamedWildCards TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11385#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
I'm assuming your `:: ...` in comment:3 are meant to be inferred, not
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
#11385: Unify named wildcards in different type applications -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | NamedWildCards TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Replying to [comment:5 goldfire]: part of what the user writes. Yes Replying to [comment:5 goldfire]: the others.
... But I think it's all OK.
Great! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11385#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11385: Unify named wildcards in different type applications -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | NamedWildCards TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Trying to wrap the [https://hackage.haskell.org/package/reflection reflection] API without `Proxy`, is there a way to implement this without visible type abstraction? This is `reflect` {{{#!hs 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 {{{#!hs reify 10 $ \p -> reflect p + reflect p }}} to be written as `↓`? {{{#!hs reify_ 10 $ \ @p -> reflect_ @p + reflect_ @p }}} ---- Minimal `reflection` API: {{{#!hs {-# 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 #-} }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11385#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11385: Unify named wildcards in different type applications -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | NamedWildCards TypeApplications 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: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * related: => #11350 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11385#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11385: Unify named wildcards in different type applications -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | NamedWildCards TypeApplications 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: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11385#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11385: Unify named wildcards in different type applications -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: duplicate | NamedWildCards TypeApplications 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: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * resolution: => duplicate Comment: OK well I'll close this one them, in favour of #11350 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11385#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC