The Coq mailing list

[James McKinna <james.mckinna AT st-andrews.ac.uk>]

Further to Conor's reply:

> What's so bad about K anyway? [etc.]

I had the impression, from Daria Walukiewiecz' (spelling?)
presentation at TYPES'03 in Torino, that JMeq, together with the
single J+K-like reduction rule for eliminating JMeq which Conor
and I give in "The View from the Left" is, in fact, perfectly OK
with regard to CiC+JMeq being SN. I would welcome confirmation or
rebuttal of this folkloric conjecture from readers of this list,
who probably know Daria's work better than I do. 

This being so, there really is no need for anyone to get upset
about "axioms", or rather, this particular axiom. All the
constructors and eliminators of type theory as we know it are
"axioms", simply ones in the presence of which we still have a
consistency proof for the logic ... with the corresponding notion
of canonical form being built up out of some of these witnesses
to axioms, viz. the constructors. If one were to change the
conversion relation for CiC+JMeq to reflect this (and Daria's
proof of SN suggests that we could), canonical forms of proofs of
JMeq would, in the empty context, be refl(t) for some term t
(also in canonical form etc.)

... as to writing programs which have dependent types, well: 

a) yes it's an obvious and important idea; 
b) it's not as easy as it should be in any of the current tools
we have, Coq or otherwise, as this discussion and many other
similar ones over recent years on this list, and others, have
shown; 
c) to do it in Coq, as Conor and I do in epigram, we might have
to accept the possibility of breaking the current paradigm in Coq
of extraction to ocaml, or else extending it to embrace the
non-Hindley-Milner typable programs which become available.

Alas, I can't attend Pierre Letouzey's seminar at ENS-Cachan next
Tuesday, to learn how Coq's extraction works these days, and thus
how it might operate on non-HM-typable programs. I would warmly
welcome the news from ocaml and Coq extraction experts to the
effect that ocaml's type system and/or the extraction mechanism
can cope with such things. 

For the vector/matrix examples, things are a bit simpler: the
length indices to the types are excluding (cf. zip) impossible
cases during inversion/pattern matching, because the constructor
forms of vectors are exactly correlated with the constructor
forms of naturals, as Conor, and Venanzio each have pointed out,
for different reasons, and to different effect. At the cost of
not-necessarily exhaustive list patterns, such functions may be
represented in ML-like languages: presumably June's listn_bin_op
could extract OK to the zip-like function 

fun   zip_bin_op f   []      []    =         []
    | zip_bin_op f (a::as) (b::bs) = (f a b) :: (zip_bin_op f as
bs)

or even

fun zip_bin_op f   0     []      []    =         []
  | zip_bin_op f (n+1) (a::as) (b::bs) = (f a b) :: (zip_bin_op n
f as bs)


Whereas Conor's epigram definition of the corresponding

fun   zip_app   []      []    =       []
    | zip_app (f::fs) (a::as) = (f a) :: (zip_app fs as)

fun   zip_n   0   a =   []
    | zip_n (n+1) a = a :: (zip_n n a)

fun zip_bin_op f as bs = zip_app (zip_app (zip_n (length as) f)
as) bs

avoids having to pass (length as) explicitly, as the typechecker
can read it off from the type of as, but presumably extraction
could calculate the need for, and insert, this call to length. 

But not all examples have such straightforward dependency. That
is both a difficulty, and the reason why dependently-typed
functional programming potentially offers so much. 

Best wishes, 

James McKinna
-- 
t: +44 (0) 13 34 46 36 91 (x 36 91 internally)
f: +44 (0) 13 34 46 32 78
p: School of Computer Science, University of St. Andrews
   North Haugh,  St. Andrews, Fife KY16 9SS, SCOTLAND