A quasi-successful attempt at hacking generative module functors into Agda 2.5.3

KindOfGenerativeModuleFunctors.agda

module KindOfGenerativeModuleFunctors where
  ------------------------------------------------------------------------------

  open import Data.Product                          using (_×_; _,_)
  open import Data.Nat                              using (ℕ)
  open import Data.Bool                             using (Bool; false; true)
  open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)

  ------------------------------------------------------------------------------

  -- Module functors in Agda, as they are normally used, are applicative:

  module ApplicativeFunctor (A : Set) where
    Foo : Set
    Foo = A × ℕ

    foo₁ : Foo → A
    foo₁ (a , _) = a

    foo₂ : Foo → ℕ
    foo₂ (_ , n) = n

  module X = ApplicativeFunctor ℕ
  module Y = ApplicativeFunctor ℕ

  -- As expected, we can prove the equality of 'X.Foo' and 'Y.Foo'.

  applicativeEq : X.Foo ≡ Y.Foo
  applicativeEq = refl

  ------------------------------------------------------------------------------

  -- Since function extensionality doesn't always hold in Agda, we can make a
  -- generative module functor by adding an extra module parameter representing
  -- a unique tag.

  -- Yes, we _need_ `Bool → Bool` rather than `⊤ → ⊤` because AFAICT Agda is
  -- smart enough to figure out that that `⊤ → ⊤` only has one inhabitant,
  -- and thus has function extensionality.
  module KindOfGenerativeFunctor (A : Set) (Tag : Bool → Bool) where
    abstract
      Bar : Set
      Bar = A × ℕ

      mkBar : A → ℕ → Bar
      mkBar a n = (a , n)

      bar₁ : Bar → A
      bar₁ (a , _) = a

      bar₂ : Bar → ℕ
      bar₂ (_ , n) = n

  -- This is a bit wordy, but macros might be able to help with that :^)
  module P = KindOfGenerativeFunctor ℕ (λ { false → false; true → true })
  module Q = KindOfGenerativeFunctor ℕ (λ { false → false; true → true })

  -- Now for the punchline:

  -- -- This gives an error, which is what we want for generative modules!
  -- kindOfGenerativeEq : P.Bar ≡ Q.Bar
  -- kindOfGenerativeEq = refl

  -- -- However, this also gives an error. I think this makes sense, since we
  -- -- are mainly exploiting the fact that Agda can't prove equality of
  -- -- functions, so it is unsurprising that Agda also can't prove their
  -- -- inequality.
  -- kindOfGenerativeNotEq : P.Bar ≢ Q.Bar
  -- kindOfGenerativeNotEq refl

  -- It might be possible to do truly generative modules using some combination
  -- of the generativity of λ, postulates, macros, and/or rewriting.
  -- I'm not sure.

  ------------------------------------------------------------------------------