On 14 Jun 2006, at 11:23, Yong Luo wrote:
By harmless, I mean the good properties such as Strong Normalisation,
Church-Rosser, Logical Consistency etc still hold if we allow
partially
defined functions.
The answers for other questions can be found in my paper (a new
version).
Constructive comments and suggestions are welcome.
http://www.cs.kent.ac.uk/people/staff/yl41/TPF.ps
So far, I am not motivated to read your paper. To be convincing you'd
have to address Conor's points here even though
I recommend another course of action below.
Basically, Conor is saying that undecidability of your problem is not
relevant because it is irrelevant in
practice. Moreover, he points out that pattern-matching by splitting
is decidable and this is implemented
in Epigram. You have given an example of a function which cannot be
defined by spltting, but Conor has
argued that this is practically irrelevant. He has also pointed out
that there are huge practical problems with your
approach, e.g. that you have to decide inhabitance to keep the theory
consistent.
My impression is that you either don't read or don't understand
Conor's points. Maybe you should go back and
do your homework before writing more emails.
Cheers,
Thorsten
Yong
----- Original Message -----
From: "Conor McBride" <[EMAIL PROTECTED]>
To: <epigram@durham.ac.uk>
Sent: Wednesday, June 14, 2006 10:02 AM
Subject: Re: [Epigram] Partially defined functions and Pattern
matching
Hello again
Yong Luo wrote:
Hi all,
Let me restate the reasons of introducing the concept of "partially
defined
functions".
1. One would like to introduce functions by pattern matching.
That's not in doubt. But when you have the Epigram set-up, with
elaboration from a high-level source language to a low-level core,
you
need to consider where pattern matching belongs. Our position has
been
that adding pattern matching to the core theory is an unnecessary
complication of it. Eliminators suffice. Moreover, by basing the
high-level pattern matching on eliminators, we provide a language of
explanation for coverings which is not restricted to constructor
patterns, and we also deliver our interactive mode of programming
without having to try too hard.
2. Full covering is an undecidable problem.
You insist on repeating this. What you mean by 'Full covering' may be
undecidable, but it is not the problem which we face. Checking
Epigram
programs for covering is perfectly decidable, and as I've pointed
out on
numerous occasions, programs which only involve /constructor/ case
analysis can be flattened to a sequence of equations and refutations.
However, with the concept of
partiality, it is not a problem any more because partially defined
functions
are harmless.
What do you mean by 'harmless' here? Leaving aside (for a moment)
your
requirement that a machine decide type inhabitation, let's see what
you're proposing. In effect, you want to equip a language of total
functions with a 'junk' operator
pred (suc n) = n
pred zero = junk
only your syntax for the junk operator is to omit the line entirely.
Your condition for deploying the junk operator is that there must
be a
term (in the approriate context) of the return type. In a total
language, programmers are free to do this, provided they make up
their
own junk, but you want to make it up for them. Do you maintain
that junk
is harmless as long as it's well-typed junk? The 'garbage in garbage
out' policy used to be respectable, but if you want to prove anything
about your programs, you spend half your life proving that what
you got
out doesn't matter because what you put in was garbage. That's why we
try to give programs more precise types in the first place. Can I
write
a function
tail : (X : *, n : Nat) Vec X n -> Vec X (pred n)
?
Returning to the question of type inhabitation, and whether or not
it's
equivalent to the covering problem, let me just ask you how you
tell if
the empty program is a valid (partial) definition of type A ->
Empty ?
Two more examples are in the following. The inhabitation of ....-
> Nat is
obvious, and it is unnecessary to check pattern coverage. See more
details
on:
http://www.cs.kent.ac.uk/people/staff/yl41/TPF.ps
I see that your patterns are constructor forms. Can you implement the
eliminators for inductive families in this language?
f :: Nat -> Nat -> Nat -> Nat
f 0 0 0 = 1
f 0 (succ y) z = g1 y z
f (succ x) y 0 = g2 x y
f x 0 (succ z) = g3 x z
f (succ x) (succ y) (succ z) = f (succ x) (succ y) z +
f (succ x) y (succ z) +
f x (succ y) (succ z)
where g1 g2 and g3 were defined beforehand.
That's recognisably a total function. Why do we need to consider
partial
functions to allow this definition? Your example does raise the
question
of whether making the above equations hold definitionally is
sufficiently desirable to motivate adding pattern matching to the
core
theory. One can have pattern matching without partial functions.
Why do
you persist in arguing for both as if they are inseparable?
Nested patterns:
np :: List (List Nat)-> Nat -> Nat
np (nil (List Nat)) n = n
np (cons (List Nat) (nil Nat) xss) n = np xss n
np (cons (List Nat) (cons Nat x xs) xss) = np (cons (List Nat)
xs xss)
(succ n)
In Haskell, one can write np as follows.
np :: [[Int]] -> Int -> Int
np [] n = n
np ([]:xss) n = np xss n
np ((x:xs):xss) n = np (xs:xss) (n+1)
What was supposed to be the problem here? The patterns are
straightforwardly a covering. The recursion is not quite
structural (in
the usual sense) because (cons xs xss) is not guarded by
constructors in
(cons (cons x xs) xss), but it's still explicable in terms of rec,
thus:
np xss n <= rec xss {
np nil n => n
np (cons xs xss') n <= rec xs {
np (cons nil xss') n => np xss' n
np (cons (cons x xs') xss') => np (cons xs' xss') (suc n) }}
Just as you're advocating a fixed external implementation of
inhabitation to justify function admissibility, you're also
advocating a
fixed external criterion for termination checking. I would much
prefer
to support a checkable language of evidence for both.
All the best
Conor
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.
