[Agda] Leibniz & Co (and no Unicode)

[Sebastian Hanowski]

 I  apologize  for  throwing entity  encodings  at  you.  Cutting  edge
programming  languages   bring  their  own   demands  on communication
technology.  Whilst I  had been  relatively lucky,  for my e-mail setup
left epigram formatting intact, it seems I'm worse off with unicode.

So I  rely on Thorsten  overcoming the  'ASCII vs. greek  dichotomy'.
UTF-8 character encoding won't do for me :)

Cheers,
Sebastian
 

My mail again, if you allow:


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 CoList (A : Set) : Set where
  CoNil : CoList A
  CoCons : A -> CoList A -> CoList A

        given a coinductive equality predicate

codata EqCoList : {A : Set} -> CoList A -> CoList A -> Set1 where
  EqCoNil : {A : Set} -> EqCoList {A} CoNil CoNil
  EqCoCons : {A : Set}{x y : A}{xs ys : CoList A} -> Eq x y -> EqCoList xs ys -> EqCoList (CoCons x xs) (CoCons y ys)

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

leibnixCo : {A : Set} -> (P : CoList A -> Set) -> (xs ys : CoList A) -> EqCoList xs ys -> P xs -> P ys
leibnixCo P  CoNil        (CoCons _ _)   ()               _
leibnixCo P (CoCons x xs)  CoNil         ()               _
leibnixCo P  CoNil         CoNil         EqNil?           pxs = pxs
leibnixCo P (CoCons x xs) (CoCons y ys) (EqCoCons xy xsys) pxs =
                                    leibnixCo (\l -> P (CoCons y l)) xs ys xsys (xy (\z -> P (CoCons z xs)) pxs)


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

 I think the  trouble with leibnixCo 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