The effect intensionality has on Functors

funext_functor.fm

import Relation.Binary
import Relation.Equality

// identity function
id : {~A : Type, x:A} -> A
  x

// composition function
compose : {~A : Type, ~B : Type, ~C : Type, g : B -> C, f : A -> B, x : A} -> C
  g(f(x))
  
// A functor without laws
T UnlawfulFunctor {F : Type -> Type}
| unlawful_functor
  { map : {~A : Type , ~B : Type , f : A -> B, x : F(A)} -> F(B)
  }

// unary function wrapper
Fun : {A : Type, B : Type} -> Type
  A -> B

// binary function wrapper
Fun2 : {A : Type, B : Type, C : Type} -> Type
  A -> B -> C

// we can use the same UnlawfulFunctor for both unary and binary functions from domain R

unlawful_fun : {R : Type} -> UnlawfulFunctor(Fun(R))
  unlawful_functor(~Fun(R), compose(~R))

unlawful_fun2 : {R : Type, S : Type} -> UnlawfulFunctor(Fun2(R,S))
  unlawful_functor(~Fun2(R,S), cmp2(~R,~S))

cmp2 : {~A : Type, ~B : Type, ~C : Type, ~D : Type
       , g : C -> D, fab : A -> B -> C
       } -> A -> B -> D
  {a,b} g(fab(a,b))

// now let's try to add a functor law

T Functor {F : Type -> Type}
| functor
  { map : {~A : Type , ~B : Type , f : A -> B, x : F(A)} -> F(B)
  , identity : {~A : Type , fa : F(A)} -> map(~A, ~A, id(~A),fa) == fa
  // we're going to ignore the composition rule for now
  }

functor.fun : {R : Type} -> Functor(Fun(R))
  functor(~Fun(R), compose(~R), ?id)

// Hole found: 'id'
// - With goal...
//   {~A : Type, fa : Fun(R, A)} -> compose(~R, ~A, ~A, id(~A), fa) == fa

// we can't make Functor(Fun(R) because we can't prove `==` on Fun(R, A)


// let's define a special Functor for unary functions
T Functor1 {F : Type -> Type}
| functor1
  { map : {~A : Type , ~B : Type , f : A -> B, x : F(A)} -> F(B)
  , identity : {~A : Type , fa : F(A), x : A} -> map(~A, ~A, id(~A),fa)(x) == fa(x)
  }

// this works
functor1.fun : {R : Type} -> Functor1(Fun(R))
  functor1(~Fun(R), compose(~R), id1(~R))

id1 :
  { ~A : Type
  , ~B : Type
  , fa : Fun(A, B)
  , x : B
  } -> compose(~A, ~B, ~B, id(~B), fa)(x) == fa(x)
  refl(~fa(x))

// But if we try to do this for
functor1.fun2 : {R : Type, S : Type} -> Functor1(Fun2(R,S))
  functor1(~Fun2(R,S), cmp2(~R,~S), ?id)

// Hole found: 'id'
// - With goal...
//  {~A : Type, fa : Fun2(R, S, A), x : A} ->
//    cmp2(~R, ~S, ~A, ~A, id(~A), fa, x) == fa(x)

// we run into the same problem with == which we can't prove over fa(x) :: S -> A

// We can curry a binary functor
Fun2C : {A : Type, B : Type, C : Type} -> Type
  [:A, B] -> C

cmp2c : {~A : Type, ~B : Type, ~C : Type, ~D : Type
       , g : C -> D, fab : [:A, B] -> C
       } -> [:A, B] -> D
  {a} g(fab(a))


// And that works

functor1.fun2c : {R : Type, S : Type} -> Functor1(Fun2C(R,S))
  functor1(~Fun2C(R,S), cmp2c(~R,~S), id2(~R,~S))

id2 :
  { ~R : Type
  , ~S : Type
  , ~A : Type
  , fa : Fun2C(R,S,A)
  , x : A
  } -> cmp2c(~R, ~S, ~A, ~A, id(~B), fa)(x) == fa(x)
  refl(~fa(x))

// Or we could define a special functor for binary functions

T Functor2 {F : Type -> Type -> Type}
| functor2
  { map : {~A : Type , ~B : Type, ~C : Type, f : B -> C, x : F(A,B)} -> F(A,C)
  , identity :
      {~A : Type
      , ~B : Type
      , fab : F(A,B)
      , x : A
      , y : B
      } -> map(~A, ~A, id(~A),fa)(x,y) == fa(x,y)
  }

// I won't construct this for Fun2, but you get the idea

// So with intensional ==, we can't reuse the same lawful functor type for any arity funtion.
// We either need a special Functor for each arity 
// or we need to uncurry the functions to unary
// Or we just use unlawful functors
// Or we use setoids
// Or we figure out how to construct extensional equality

// The same pattern applies for Applicative, Monad, etc.