Is there a way to define `Refl` in Morte?

[ChristopherKing42]

Can a Refl like type be defined in Morte for demonstrating equality between two terms?

http://stackoverflow.com/questions/36181738/refl-type-in-calculus-of-constructions

(In general, can GADTs be encoded in Morte?)

[Gabriella439]

Yes, you can encode Refl in morte.

First, for simplicity, let's assume that we already have the following external definitions as local files so that we can reference them using morte's import system:

$ cat Nat
forall (Nat : *) -> forall (Succ : Nat -> Nat) -> forall (Zero : Nat) -> Nat
$ cat Succ
    \(n : #Nat )
->  \(Nat : *)
->  \(Succ : Nat -> Nat)
->  \(Zero : Nat)
->  Succ (n Nat Succ Zero)
$ cat Zero
    \(Nat : *)
->  \(Succ : Nat -> Nat)
->  \(Zero : Nat)
->  Zero
$ cat '(+)'
    \(m : #Nat )
->  \(n : #Nat )
->  \(Nat : *)
->  \(Succ : Nat -> Nat)
->  \(Zero : Nat)
->  m Nat Succ (n Nat Succ Zero)
$ cat One
#Succ #Zero

Now, here is how I would prove in morte that 1 + 0 = 0 + 1 using Refl:

    \(Refl : #Nat -> #Nat -> *)
->  \(MkRefl : forall (n : #Nat ) -> Refl n n)
->  (   \(x : Refl (#(+) #One #Zero ) (#(+) #Zero #One ))
    ->  x
    )

    (MkRefl #One )

The above program type-checks, but if you change the type parameters to Refl to types that do not match such as this program:

    \(Refl : #Nat -> #Nat -> *)
->  \(MkRefl : forall (n : #Nat ) -> Refl n n)
->  (   \(x : Refl (#(+) #One #One ) (#(+) #Zero #One ))
    ->  x
    )

    (MkRefl #One )

... then type-checking will fail.

I can also tie this into your other question about proving commutativity. You cannot use the above Refl mechanism to prove commutativity. For example, the following program does not type-check:

    \(Refl : (#Nat -> #Nat -> #Nat ) -> (#Nat -> #Nat -> #Nat ) -> *)
->  \(MkRefl : forall (n : #Nat -> #Nat -> #Nat ) -> Refl n n)
->  (   \(x : Refl (\(x : #Nat ) -> \(y : #Nat ) -> #(+) x y)
                   (\(x : #Nat ) -> \(y : #Nat ) -> #(+) y x) )
    ->  x
    )

    (MkRefl (\(x : #Nat ) -> \(y : #Nat ) -> #(+) x y))

... and fails with an error message stating that the commuted additions are not equal:

$ morte < example
...
Error: Function applied to argument of the wrong type

Expected type: Refl (λ(x : ∀(Nat : *) → ∀(Succ : Nat → Nat) → ∀(Zero : Nat) → Nat) → λ(y : ∀(Nat : *) → ∀(Succ : Nat → Nat) → ∀(Zero : Nat) → Nat) → λ(Nat : *) → λ(Succ : Nat → Nat) → λ(Zero : Nat) → x Nat Succ (y Nat Succ Zero)) (λ(x : ∀(Nat : *) → ∀(Succ : Nat → Nat) → ∀(Zero : Nat) → Nat) → λ(y : ∀(Nat : *) → ∀(Succ : Nat → Nat) → ∀(Zero : Nat) → Nat) → λ(Nat : *) → λ(Succ : Nat → Nat) → λ(Zero : Nat) → y Nat Succ (x Nat Succ Zero))
Argument type: Refl (λ(x : ∀(Nat : *) → ∀(Succ : Nat → Nat) → ∀(Zero : Nat) → Nat) → λ(y : ∀(Nat : *) → ∀(Succ : Nat → Nat) → ∀(Zero : Nat) → Nat) → λ(Nat : *) → λ(Succ : Nat → Nat) → λ(Zero : Nat) → x Nat Succ (y Nat Succ Zero)) (λ(x : ∀(Nat : *) → ∀(Succ : Nat → Nat) → ∀(Zero : Nat) → Nat) → λ(y : ∀(Nat : *) → ∀(Succ : Nat → Nat) → ∀(Zero : Nat) → Nat) → λ(Nat : *) → λ(Succ : Nat → Nat) → λ(Zero : Nat) → x Nat Succ (y Nat Succ Zero))

However, you can use morte to prove associativity and identity. For example, all of the following programs type-check:

    \(  Refl
    :   (#Nat -> #Nat -> #Nat -> #Nat ) -> (#Nat -> #Nat -> #Nat -> #Nat ) -> *
    )
->  \(MkRefl : forall (n : #Nat -> #Nat -> #Nat -> #Nat ) -> Refl n n)
->  (   \(  x
        : Refl
            (\(x : #Nat ) -> \(y : #Nat ) -> \(z : #Nat ) -> #(+) x (#(+) y z))
            (\(x : #Nat ) -> \(y : #Nat ) -> \(z : #Nat ) -> #(+) (#(+) x y) z)
        )
    ->  x
    )

    (MkRefl (\(x : #Nat ) -> \(y : #Nat ) -> \(z : #Nat ) -> #(+) x (#(+) y z)))

    \(Refl : (#Nat -> #Nat ) -> (#Nat -> #Nat ) -> *)
->  \(MkRefl : forall (n : #Nat -> #Nat ) -> Refl n n)
->  (   \(x : Refl (\(x : #Nat ) -> #(+) x #Zero )
                   (\(x : #Nat ) -> x ) )
    ->  x
    )

    (MkRefl (\(x : #Nat ) -> x))

    \(Refl : (#Nat -> #Nat ) -> (#Nat -> #Nat ) -> *)
->  \(MkRefl : forall (n : #Nat -> #Nat ) -> Refl n n)
->  (   \(x : Refl (\(x : #Nat ) -> #(+) #Zero x )
                   (\(x : #Nat ) -> x ) )
    ->  x
    )

    (MkRefl (\(x : #Nat ) -> x))

I believe GADTs can be encoded in terms of Refl + existential quantification and since existential quantification can also be encoded then I believe you can encode GADTs in morte, too, although it might not be very pretty.

[ChristopherKing42]

GADTs actually can be encoded in a way similar to REFL I'm pretty sure.

[Gabriella439]

I will go ahead and mark this closed since I believe the original question was answered, but feel free to reopen if you have any additional questions

[lukaszlew]

Typing Dynamic Typing section 3 and this presentation slide 22 are relevant. Both suggest that the Church encoding of 'Identity types' is Leibnitz equality. @Gabriel439 can you comment on that? Also could you comment on how does you commutativity and associativity proofs work without induction principles? Induction principles are traditionally added to the languages like CoIC through inductive types.

[Gabriella439]

@lukaszlew: Yeah, using Leibniz equality seems much simpler. I didn't know about it until you pointed it out