[GHC] #11638: referring to the existential type from a GADT pattern match with a type application
#11638: referring to the existential type from a GADT pattern match with a type application -------------------------------------+------------------------------------- Reporter: rwbarton | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple TypeApplications | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #11387 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Currently I can define a GADT like {{{ data T where MkT :: forall a. (Num a, Show a) => T }}} but it's useless on two counts: * At a use of the constructor `MkT`, I can't specify what type `a` I want to pack dictionaries for. (In fact the declaration is an error unless either the constraints are defaultable (as in the case above) or AllowAmbiguousTypes is enabled.) * At a pattern match against `MkT`, I have no way to refer to the type for which dictionaries were packed. The solution is to add a field of type `Proxy a` (possibly strict/unpacked) or `Proxy# a` to `MkT`. But these options are all a bit verbose and each have minor drawbacks. I had hoped that TypeApplications would address the two points above directly. * At a use of the constructor `MkT`, specify the type with a type application `MkT @a`. This part works as of 90f35612f16ff9cb2466cc936f12e748402abb85. * At a pattern match against `MkT`, I would like to be able to match the type directly like this: {{{ f :: T -> String f t = case t of MkT @a -> show (0 :: a) }}} This is the feature request. Note that, while this may be stressful for the parser due to as-patterns, I don't think there is any actual ambiguity as long as (1) type applications only appear on constructors, not variables, and (2) all type applications appear before any value-level fields of the constructor. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11638 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11638: referring to the existential type from a GADT pattern match with a type application -------------------------------------+------------------------------------- Reporter: rwbarton | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11387 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I actually implemented this partially. But there are devilish details (numbered only for reference): 1. We only pattern-match on ''existentials'', never ''universals''. That is, if we have {{{#!hs data T1 a where MkT1 :: a -> b -> T1 a }}} Using `MkT1` as an expression: we could say `MkT1 @Int @Bool 5 True`. But as a pattern, we would have to omit the first argument: `foo (MkT1 @b x y)`. This is confusing. I suppose we could include the universals in the pattern-match, but they would have to be underscores or an exact match for the inferred instantiation of the universal type variable. 2. Users can reorder the variables in a data constructor, making point (1) even worse: {{{#!hs data T2 a where MkT2 :: forall b a. a -> b -> T2 a }}} Note the explicit `forall` reordering the variables. So it's not necessarily a prefix of variables that get dropped. 3. Naturally, any visible type patterns would have to bind only bare type variables, never match against types. Otherwise, we've lost type erasure and parametricity. 4. Do visible type patterns extend beyond data constructors? To wit: {{{#!hs foo :: forall a. a -> a foo @b x = (x :: b) }}} Is that accepted? What about {{{#!hs (\ @a x -> (x :: a)) :: forall b. b -> b }}} It sure would be nice to be able to do this -- it would make continuation-passing style with fancy types easier. There are solutions here, of course, but I just wanted to write down a few thoughts while I still remember them. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11638#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11638: referring to the existential type from a GADT pattern match with a type application -------------------------------------+------------------------------------- Reporter: rwbarton | Owner: Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: duplicate | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11387 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * resolution: => duplicate Comment: This is subsumed by #11350. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11638#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC