Parametricity as erasure

b.hs

{-
  "Goal": translate this to Idris
  
  Name    Meaning

  forall  Parametric universal
  pi      Nonparametric universal
  exists  Parametric existential
  sigma   Nonparametric existential


  Note that
  exists t. a = forall r. (forall t. a -> r) -> r

  And, I think,
  sigma t. a = forall r. (pi t. a -> r) -> r
  
  where t is a free variable in a.


  Table of examples:
  
  Name  Parametric?  Type
  pu1   yes          universal
  nu1   no           universal
  pe1   yes          existential
  ne1   no           existential
  pe2   yes          existential
  ne2   no           existential
-}

pu1 :: forall t. t -> t
pu1 = id

nu1 :: pi t. t -> t
nu1 @Int 3 = 4
nu1 @_   x = x

data Void -- No constructors

pe1 :: exists (a :: Char). Int
pe1 = 3

ne1 :: sigma (a :: Char). Int
ne1 = 'r' ** 3

pe2 :: exists (a :: Void). Int
pe2 = 10

ne2 :: sigma (a :: Void). Int
ne2 = ?a ** 10 -- This is impossible to define because there are no values
               -- of type Void