open import 1Lab.Type.Sigma
open import 1Lab.Type.Pi
open import 1Lab.Equiv
open import 1Lab.Type

module 1Lab.Type.Pi.Currying where

Currying and uncurrying automationπŸ”—

This module contains proof automation for passing between curried and uncurried Ξ  types.

CurryingπŸ”—

The core of our currying automation is the following typeclass, which decomposes a type into a Ξ  type.

record Curried {β„“} (A : Type β„“) (β„“d β„“f : Level) : Type (β„“ βŠ” lsuc β„“d βŠ” lsuc β„“f) where
  no-eta-equality
  field
    Dom : Type β„“d
    Cod : Dom β†’ Type β„“f
    eqv : ((d : Dom) β†’ Cod d) ≃ A

The only interesting instances of Curried check to see if is an iterated Ξ  type, and shuffle over elements of the codomain into a Ξ£ in the domain.

instance
  Curried-Ξ 
    : βˆ€ {β„“ β„“' β„“'' β„“d β„“f} {A : Type β„“} {B : A β†’ Type β„“'} {C : (a : A) β†’ B a β†’ Type β„“''}
    β†’ ⦃ _ : βˆ€ {a} β†’ Curried ((b : B a) β†’ C a b) β„“d β„“f ⦄
    β†’ Curried ((a : A) (b : B a) β†’ C a b) (β„“d βŠ” β„“) β„“f
  Curried-Ξ  {A = A} ⦃ c ⦄ .Curried.Dom = Ξ£[ a ∈ A ] (Curried.Dom (c {a}))
  Curried-Ξ  {A = A} ⦃ c ⦄ .Curried.Cod (a , d) = Curried.Cod c d
  Curried-Ξ  {A = A} ⦃ c ⦄ .Curried.eqv = curry≃ βˆ™e Ξ -ap-cod Ξ» a β†’ Curried.eqv c

  Curried-Ξ '
    : βˆ€ {β„“ β„“' β„“'' β„“d β„“f} {A : Type β„“} {B : A β†’ Type β„“'} {C : (a : A) β†’ B a β†’ Type β„“''}
    β†’ ⦃ _ : βˆ€ {a} β†’ Curried ((b : B a) β†’ C a b) β„“d β„“f ⦄
    β†’ Curried ({a : A} (b : B a) β†’ C a b) (β„“d βŠ” β„“) β„“f
  Curried-Ξ ' {A = A} ⦃ c ⦄ .Curried.Dom = Ξ£[ a ∈ A ] (Curried.Dom (c {a}))
  Curried-Ξ ' {A = A} ⦃ c ⦄ .Curried.Cod (a , d) = Curried.Cod c d
  Curried-Ξ ' {A = A} ⦃ c ⦄ .Curried.eqv = curry≃ βˆ™e Ξ -impl≃ βˆ™e Ξ '-ap-cod Ξ» a β†’ Curried.eqv c

Finally, we have an INCOHERENT base case that will match only when we have run out of iterated Ξ  types.

  Curried-default
    : βˆ€ {β„“ β„“'} {A : Type β„“} {B : A β†’ Type β„“'}
    β†’ Curried ((a : A) β†’ B a) β„“ β„“'
  Curried-default {A = A} {B = B} .Curried.Dom = A
  Curried-default {A = A} {B = B} .Curried.Cod = B
  Curried-default {A = A} {B = B} .Curried.eqv = id≃
  {-# INCOHERENT Curried-default #-}

Now that we’ve got our instances in place, we can use instance arguments to compute the fully curried version of a type.

Curry : βˆ€ {β„“ β„“d β„“f} β†’ (A : Type β„“) β†’ ⦃ C : Curried A β„“d β„“f ⦄ β†’ Type (β„“d βŠ” β„“f)
Curry A ⦃ C ⦄ = (x : Curried.Dom C) β†’ Curried.Cod C x
{-# NOINLINE Curry #-}

We also expose the equivlance between the original type and it’s curried form.

curry!
  : βˆ€ {β„“ β„“d β„“f}
  β†’ {A : Type β„“}
  β†’ ⦃ C : Curried A β„“d β„“f ⦄
  β†’ A ≃ Curry A
curry! ⦃ C ⦄ = Curried.eqv C e⁻¹
{-# NOINLINE curry! #-}

UncurryingπŸ”—

The uncurrying typeclass is identical to the currying typeclass in all but name.

record Uncurried {β„“} (A : Type β„“) (β„“d β„“f : Level) : Type (β„“ βŠ” lsuc β„“d βŠ” lsuc β„“f) where
  no-eta-equality
  field
    Dom : Type β„“d
    Cod : Dom β†’ Type β„“f
    eqv : ((d : Dom) β†’ Cod d) ≃ A

However, the instances for Uncurried go in the opposite direction.

instance
  Uncurried-Ξ 
    : βˆ€ {β„“ β„“' β„“'' β„“d β„“f} {A : Type β„“} {B : A β†’ Type β„“'} {C : Ξ£ A B β†’ Type β„“''}
    β†’ ⦃ _ : βˆ€ {a} β†’ Uncurried ((b : B a) β†’ C (a , b)) β„“d β„“f ⦄
    β†’ Uncurried ((ab : Ξ£ A B) β†’ C ab) β„“ (β„“d βŠ” β„“f)
  Uncurried-Ξ  {A = A} ⦃ c ⦄ .Uncurried.Dom = A
  Uncurried-Ξ  {A = A} ⦃ c ⦄ .Uncurried.Cod a = (d : Uncurried.Dom (c {a})) β†’ Uncurried.Cod (c {a}) d
  Uncurried-Ξ  {A = A} ⦃ c ⦄ .Uncurried.eqv = Ξ -ap-cod (Ξ» a β†’ Uncurried.eqv c) βˆ™e curry≃ e⁻¹

  Uncurried-default
    : βˆ€ {β„“ β„“'} {A : Type β„“} {B : A β†’ Type β„“'}
    β†’ Uncurried ((a : A) β†’ B a) β„“ β„“'
  Uncurried-default {A = A} {B = B} .Uncurried.Dom = A
  Uncurried-default {A = A} {B = B} .Uncurried.Cod = B
  Uncurried-default {A = A} {B = B} .Uncurried.eqv = id≃

We expose a similar API for uncurrying.

Uncurry : βˆ€ {β„“ β„“d β„“f} β†’ (A : Type β„“) β†’ ⦃ C : Uncurried A β„“d β„“f ⦄ β†’ Type (β„“d βŠ” β„“f)
Uncurry A ⦃ C ⦄ = (x : Uncurried.Dom C) β†’ Uncurried.Cod C x
{-# NOINLINE Uncurry #-}

uncurry!
  : βˆ€ {β„“ β„“d β„“f}
  β†’ {A : Type β„“}
  β†’ ⦃ C : Uncurried A β„“d β„“f ⦄
  β†’ A ≃ Uncurry A
uncurry! ⦃ C ⦄ = Uncurried.eqv C e⁻¹
{-# NOINLINE uncurry! #-}