The Coq mailing list

[Conor McBride <conor AT cs.rhul.ac.uk>]

Evening all

Venanzio Capretta wrote:
> Hi Conor,
>
> > > I challenge you to do the same using the inductive Vector (or listn) 
> > > definition!
> By the way, you didn't beat the challenge yet! To do so you have to 
> define a function like my tuple_n_map, that is:

Will the attached do?

> Of course my challenge was to do it in Coq (with no axioms).
[..]
> In Coq we have to consider the vnil case also, introduce an extra 
> equality in the domain predicate etc... How does Epigram do it? Is its 
> type theory different and nicer, or is there an automathic translation 
> that does the dirty work for you?

Apart from having JMeq as standard, there's no significant difference in
the type theory (relevant to this issue anyway). It's the latter: there's
an automathic (is that how they spell it in the Netherlands?) translation
that does the dirty work for me. Pretty much everything Epigram does could
happen in Coq, one way or another.

> I actually used this definition in past formalizations and it seems to 
> be the easiest to use. The fact that equality is extensional didn't seem 
> to be a problem.

It really depends on what you're doing: I was proving properties about
unifiers, so I had the usual pain of showing that every property I cared
about respected extensional equality of substitutions. But what's really
cool is that my two favourite operations, vec and vapp are trivial, and
all the obvious theorems like (vapp (vec f) (vec s)) i = vec (f s) i
are actually true intensionally!

[Vectors are a monad, with vec as the eta/return, and the join being the
function which takes the diagonal of a square matrix. vapp is just the
lifting of application into this monad. vec and vapp generate all the
usual mapping and zipping operations, hence their utility for the challenge
you set. I'm also a vec/vapp bore, see
  http://www.haskell.org/pipermail/haskell/2004-July/014315.html
]

> >  What's so bad about K anyway?
> I don't have anything in particular agains K, but in general I don't 
> like axioms. When you are forced to use an axiom it means that your type 
> theory is not doing the job. One should rather rething the system so 
> that the desired properties are "structural" rather that axiomatic.

To some extent, the type theory as it stands is not doing its job, because
it fails to support K, which _is_ a structural property, namely that
every inhabitant of x = x is made by the constructor of x = x.
Just assuming K isn't enough: you also need its computation rule.
K really gets used in the elaboration of pattern matching, so it shouldn't
get stuck.

The trouble with the type theory is this: when we declare a family of
datatypes, we don't get a family of eliminators (which is what pattern
matching amounts to), just an eliminator for the family. Equality allows you
to specialise the whole-family eliminator to the eliminator for a given
subfamily (a vector of any length as long as it's equal to zero, and so on).
But to solve the resulting equations, you need the structural properties
of equality, and one of them is missing...

> In the case under study, Pierre Casteran showed how to do things without 
> assuming axioms, if you can do without them you should.

Yes of course. And as Cuihtlauac points out, quite a lot of the instances
of K which you need in practice turn out to be derivable. So any K-based
pattern matching technology could still have a powerful 'purist mode'.
But in this case, it's the absence of K rather than the presence which I
think requires the peculiar justification. I could hop most places, but
I find walking much more natural, especially as my study is upstairs.

Cheers

Conor

--
http://www.cs.rhul.ac.uk/~conor
------------------------------------------------------------------------------
                                          (   n : Nat   !
data (---------!  where (------------! ;  !-------------!
     ! Nat : * )        ! zero : Nat )    ! suc n : Nat )
------------------------------------------------------------------------------
     ( n : Nat ;  X : * !                                         
data !------------------!                                         
     !   Vec n X : *    )                                         
                                                                  
                               ( X ;  n ;  x : X ;  xs : Vec n X !
where (-------------------! ;  !---------------------------------!
      ! vnil : Vec zero X )    !   vcons x xs : Vec (suc n) X    )
------------------------------------------------------------------------------
     (     n ;  x : X     !                
let  !--------------------!                
     ! vec _n x : Vec n X )                
                                           
     vec _ n x <= rec n                    
     { vec _ n x <= case n                 
       { vec _ zero x => vnil              
         vec _ (suc n) x => vcons x (vec x)
       }                                   
     }                                     
------------------------------------------------------------------------------
     ( fs : Vec n (S -> T) ;  ss : Vec n S !                         
let  !-------------------------------------!                         
     !        vapp fs ss : Vec n T         )                         
                                                                     
     vapp fs ss <= rec fs                                            
     { vapp fs ss <= case fs                                         
       { vapp vnil ss <= case ss                                     
         { vapp vnil vnil => vnil                                    
         }                                                           
         vapp (vcons f fs) ss <= case ss                             
         { vapp (vcons f fs) (vcons s ss) => vcons (f s) (vapp fs ss)
         }                                                           
       }                                                             
     }                                                               
------------------------------------------------------------------------------
     ( f : X -> X -> X ;  xs, ys : Vec n X ! 
let  !-------------------------------------! 
     !        vbo f xs ys : Vec n X        ) 
                                             
     vbo f xs ys => vapp (vapp (vec f) xs) ys
------------------------------------------------------------------------------
     (    xss : Vec m (Vec n X)     !                                    
let  !------------------------------!                                    
     ! vtrans xss : Vec n (Vec m X) )                                    
                                                                         
     vtrans xss <= rec xss                                               
     { vtrans xss <= case xss                                            
       { vtrans vnil => vec vnil                                         
         vtrans (vcons xs xss) => vapp (vapp (vec vcons) xs) (vtrans xss)
       }                                                                 
     }                                                                   
------------------------------------------------------------------------------
     ( S : * ;  n : Nat ;  T : * !            
let  !---------------------------!            
     !      Arity S n T : *      )            
                                              
     Arity S n T <= rec n                     
     { Arity S n T <= case n                  
       { Arity S zero T => T                  
         Arity S (suc n) T => S -> Arity S n T
       }                                      
     }                                        
------------------------------------------------------------------------------
     ( m, n : Nat ;  S, T : * ;  fs : Vec m (Arity S n T) !            
let  !----------------------------------------------------!            
     !   vapps m n S T fs : Arity (Vec m S) n (Vec m T)   )            
                                                                       
     vapps m n S T fs <= rec n                                         
     { vapps m n S T fs <= case n                                      
       { vapps m zero S T fs => fs                                     
         vapps m (suc n) S T fs => lam ss => vapps m n S T (vapp fs ss)
       }                                                               
     }                                                                 
------------------------------------------------------------------------------
     (   m, n : Nat ;  S, T : * ;  f : Arity S n T   !
let  !-----------------------------------------------!
     ! vmaps m n S T f : Arity (Vec m S) n (Vec m T) )
                                                      
     vmaps m n S T f => vapps m n S T (vec f)         
------------------------------------------------------------------------------