[GHC] #14859: Allow explicit impredicativity
#14859: Allow explicit impredicativity -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- In [https://mail.haskell.org/pipermail/ghc-devs/2016-September/012940.html this email] I suggested allowing a simple form of impredicativity. With a suitable extension flag (`-XExplicitImpredicativeTypes` perhaps), you woudl be allowed: * To write a polytype in a visible type argument; eg. `f @(forall a. a->a)` * To write a polytype as an argument of a type in a signature e.g. `f :: [forall a. a->a] -> Int` ''But that’s all''. A unification variable still cannot be unified with a polytype. The only way you can call a polymorphic function at a polytype is to use Visible Type Application (VTA). So using impredicative types might be tiresome. E.g. {{{ type SID = forall a. a->a xs :: [forall a. a->a] xs = (:) @SID id ( (:) @SID id ([] @ SID)) }}} In short, if you call a function at a polytype, you must use VTA. Simple, easy, predictable; and doubtless annoying. But at least it's possible. The main motivation is that we are naughtily doing this anyway in the implementation of `GeneralisedNewtypeDeriving` -- see Trac #14070 comment:23 ff. If we are doing it under the hood, we could just made it available to programmers. This is much less ambitious, and much easier to implement, than the proposed [https://www.microsoft.com/en-us/research/publication/guarded- impredicative-polymorphism/ Guarded impredicative polymorphism] (PLDI'18). This ticket just records the idea, to see what other use-cases people might want to add. Then someone would have to write a GHC proposal. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14859 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14859: Allow explicit impredicativity -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => ImpredicativeTypes -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14859#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14859: Allow explicit impredicativity -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14859#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14859: Allow explicit impredicativity -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14859#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14859: Allow explicit impredicativity -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | ImpredicativeTypes 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 RyanGlScott): Should we allow visible application of polytypes //carte blanche//? What happens when visible kind application rolls in and we can write this? {{{#!hs hm :: forall (f :: forall a. a -> a). Proxy @(forall a. a -> a) f hm = Proxy }}} The type `Proxy @(forall a. a -> a) f` seems to have a strongly impredicative flavor, but this is only a hunch. What do others think? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14859#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14859: Allow explicit impredicativity -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | ImpredicativeTypes 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 simonpj): I think it's at least ''plausible'' that explicit type application to polytypes would be OK. It would take a little work make ''sure'' it was OK, but it is, as you say, much less ambitious than "Guarded impredicative polymorphism". A good project for someone. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14859#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14859: Allow explicit impredicativity -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | ImpredicativeTypes 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): Impredicativity is perfectly fine in Core. (At least in theory. I'm sure panics await.) So giving users controlled access to it in source Haskell is safe, in that we won't launch the rockets. As we open this gate, horrors might await us on the other side, but they should all be type inference horrors, not type safety ones. I am thus in support of this direction of travel. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14859#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC