Opened 19 months ago

Last modified 11 months ago

#14859 new bug

Allow explicit impredicativity

Reported by: simonpj Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.2.2
Keywords: ImpredicativeTypes Cc: Iceland_jack, RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

In 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 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.

Change History (6)

comment:1 Changed 19 months ago by simonpj

Keywords: ImpredicativeTypes added

comment:2 Changed 19 months ago by Iceland_jack

Cc: Iceland_jack added

comment:3 Changed 18 months ago by RyanGlScott

Cc: RyanGlScott added

comment:4 Changed 11 months ago by RyanGlScott

Should we allow visible application of polytypes carte blanche? What happens when visible kind application rolls in and we can write this?

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?

comment:5 Changed 11 months ago 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.

comment:6 Changed 11 months ago 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.

Note: See TracTickets for help on using tickets.