[Agda] Leibniz & Co

[Sebastian Hanowski]

Hi all,


the advent of codata in Agda2 makes me finally want to understand some
claims from this talk by Thorsten:

        http://www.cs.nott.ac.uk/~txa/talks/types04.pdf

Given the Leibniz-encoding of equality

Eq : {A : Set} -> A -> A -> Set1
Eq {A} x y = (P : A -> Set) -> P x -> P y

        and the type of lists

data List (A : Set) : Set where
  Nil : List A
  Cons : A -> List A -> List A

        there's an inductive type corresponding to the primitive recursive equality predicate

data EqList : {A : Set} -> List A -> List A -> Set1 where
  EqNil : {A : Set} -> EqList {A} Nil Nil
  EqCons : {A : Set}{x y : A}{xs ys : List A} -> Eq x y -> EqList xs ys -> EqList (Cons x xs) (Cons y ys)

        which can be used to substitute equal lists.

leibniz : {A : Set} -> (P : List A -> Set) -> (xs ys : List A) -> EqList xs ys -> P xs -> P ys
leibniz P  Nil         (Cons _ _)  ()              _
leibniz P (Cons x xs)   Nil        ()              _
leibniz P  Nil          Nil        EqNil           pxs = pxs
leibniz P (Cons x xs) (Cons y ys) (EqCons xy xsys) pxs =
                                    leibniz (\l -> P (Cons y l)) xs ys xsys (xy (\z -> P (Cons z xs)) pxs)

        
{- I like to point out the symmetry here, you can also 'fold right' -}
leibniz' : {A : Set} -> (P : List A -> Set) -> (xs ys : List A) -> EqList xs ys -> P xs -> P ys
leibniz' P  Nil         (Cons _ _)  ()              _
leibniz' P (Cons x xs)   Nil        ()              _
leibniz' P  Nil          Nil        EqNil           pxs = pxs
leibniz' P (Cons x xs) (Cons y ys) (EqCons xy xsys) pxs =
                                     xy (\z -> P (Cons z ys)) (leibniz' (\l -> P (Cons x l)) xs ys xsys pxs)


However, though you can make useful observations about colists

codata List∞ (A : Set) : Set where
  Nil∞ : List∞ A
  Cons∞ : A -> List∞ A -> List∞ A

        given a coinductive equality predicate

codata EqList∞ : {A : Set} -> List∞ A -> List∞ A -> Set1 where
  EqNil∞ : {A : Set} -> EqList∞ {A} Nil∞ Nil∞
  EqCons∞ : {A : Set}{x y : A}{xs ys : List∞ A} -> Eq x y -> EqList∞ xs ys -> EqList∞ (Cons∞ x xs) (Cons∞ y ys)

         you can't use this to substitute equals for equals, as Thorsten remarks

leibnix∞ : {A : Set} -> (P : List∞ A -> Set) -> (xs ys : List∞ A) -> EqList∞ xs ys -> P xs -> P ys
leibnix∞ P  Nil∞        (Cons∞ _ _)   ()               _
leibnix∞ P (Cons∞ x xs)  Nil∞         ()               _
leibnix∞ P  Nil∞         Nil∞         EqNil∞           pxs = pxs
leibnix∞ P (Cons∞ x xs) (Cons∞ y ys) (EqCons∞ xy xsys) pxs =
                                    leibnix∞ (\l -> P (Cons∞ y l)) xs ys xsys (xy (\z -> P (Cons∞ z xs)) pxs)

And  I guess  the  Agda2  system marks  this  program  because it's  not
productive.

 I think the  trouble with leibnix∞ is, that it  only returns when the
data is exhausted. Which  is not a good idea for  codata. We should have
it driven  by the observation  that P makes,  i.e. returning once  P has
been fed enough input.

I'm keen to learn what observational type theory could add here. Or, can
we have a partial type checking algorithm  to get a hold of the /modulus
of continuity/ of a predicate defined on codata?

And in a type theory augmented with a notion of continuity

        http://www.cs.nott.ac.uk/~txa/talks/russell08.pdf

we  probably  could write  the  program  by  recursion directly  on  the
predicate.



Best regards,
Sebastian

_____________________________________________________________________
Der WEB.DE SmartSurfer hilft bis zu 70% Ihrer Onlinekosten zu sparen!
http://smartsurfer.web.de/?mc=100071&distributionid=000000000066