Smart Case [Re: [Agda] A puzzle with "with"]

[Andreas Abel]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Oh, Thorsten, I should have read your paper before. ;-)  But anyway, now
that I read it, I realize that I arrived at the same implementation idea
as you, which is reassuring.  [I remember you have been investigating
constraints since the MuTTI days.]

A noteworthy thought is that you can detect some inconsistent
constraints with your algorithm (the one I have also be aiming at), but
not all.  Consider the booleans with identity and negation defined by
case distinction.  Then, the constraints

  id  x = true
  not x = true

are inconsistent, but it goes unnoticed.  (A case distinction on x would
of course make it apparent.)  This is why I think that completeness of
type checking is hard to achieve even in the presence of first order
constraints.  However, of the three properties

- - soundness
- - completeness
- - termination

of type checking, completeness is the first to sacrifice.  A lack of
completeness might involve some degree of frustration to the user, but
it has to be weighted against the current frustration with "with".  The
added convenience would imho compensate for incompleteness.

@Nisse:  Surely, Agda expressions could not be translated to core
anymore, but their typing derivations could.  For instance, into a
language with explicit proofs of definitional equality everywhere, as
suggested by Freek Wiedijk.

Cheers,
Andreas

Thorsten Altenkirch wrote:
>>
>> The "magic with" meets this expectation partially by rewriting the
>> current goal.  However, the equation "bla = true" may be needed not
>> only in the goal, but otherwhere as well.  The inspect pattern
>> provides this equation as a proof which can be manipulated explicitly,
>> yet inspect is complicated to use, in the general case you have to
>> apply Josh Ko's pattern.  It is desirable that Agda considers "bla"
>> and "true" as definitionally equal.
> 
> Precisely!!!
> 
> We tried to do this in the original PiSigma paper:
> http://www.cs.nott.ac.uk/~txa/publ/pisigma.pdf
> but decided that dealing with constraint in general seems to be too
> heavy for a core language. However, I think it would be a desirable
> feature for a high level langauge like Agda. Nisse asks the right
> question - and I think such a translation is possible but not trivial.
> 
> Basically we allowed to assume certain equalities (constraints) in the
> context. It is not completely trivial to make sure that transitivity of
> equality still holds. In our implementation we always tried to maintain
> that all the constraint are normal wrt to each other.
> 
> If I remember correctly one issue was closure under xi, because this
> leads to undecidability due to having to deal with universally
> quantified constraints.
> 
> Cheers,
> Thorsten
> 
> 
> 
> 
> On 3 Jul 2009, at 10:13, Andreas Abel wrote:
> 
>> Let me add my 5 cent to this discussion.
>>
>> It seems that the "naive" user (for instance, me) expects that Agda
>> "knows" that "bla = true" in "anotherthing" when writing
>>
>> something with bla
>> ...  | true = anotherthing
>>
>> The "magic with" meets this expectation partially by rewriting the
>> current goal.  However, the equation "bla = true" may be needed not
>> only in the goal, but otherwhere as well.  The inspect pattern
>> provides this equation as a proof which can be manipulated explicitly,
>> yet inspect is complicated to use, in the general case you have to
>> apply Josh Ko's pattern.  It is desirable that Agda considers "bla"
>> and "true" as definitionally equal.
>>
>> I have played with idea by adding rewriting to MiniAgda
>>
>>  http://www.tcs.ifi.lmu.de/~abel/miniagda/
>>
>> While type checking "anotherthing", the rewrite rule "bla --> true"
>> may fire.
>>
>> For example, this enables a simple proof of  f = f . f . f  for
>> boolean functions f in MiniAgda.
>>
>> data Bool : Set
>> { true  : Bool
>> ; false : Bool
>> }
>>
>> data Id (A : Set)(a : A) : A -> Set
>> { refl : Id A a a
>> }
>>
>> -- Lemma: f x = f (f (f x))  for all f : Bool -> Bool
>> -- Proof by cases on x, f true, and f false
>> fun tripleF : (f : Bool -> Bool) -> (x : Bool) -> Id Bool (f x) (f (f
>> (f x)))
>> { tripleF f true = case f true
>>  { true -> refl Bool true
>>  ; false -> case f false
>>    { true  -> refl Bool false
>>    ; false -> refl Bool false
>>    }
>>  }
>> ; tripleF f false = case f false
>>  { true -> case f true
>>    { true -> refl Bool true
>>    ; false -> refl Bool true
>>    }
>>  ; false -> refl Bool false
>>  }
>> }
>>
>> The same proof cannot be done with "magic with", since, the equations
>> like "f true = true" have to be used more than once in the goal.  [A
>> proof with inspect would certainly be possible.]
>>
>> Case is limited to inductive /types/ at the moment, for inductive
>> families one would need a combination of "with" and rewriting.
>>
>> Another example: Insertion into sorted lists.  Here I need to compare
>> n and m with leq n m and in case true, I need to embed a proof of leq
>> n m == true into my sorted list structure by passing it as an argument
>> to scons. Since this equation holds definitionally, the proof is
>> "triv"ial.  Here is an excerpt, I include the full code.
>>
>> data SList : Nat -> Set
>> { snil  : SList zero
>> ; scons : (m : Nat) -> (n : Nat) -> True (leq n m)  -> SList n -> SList m
>> }
>>
>> fun insert : (m : Nat) -> (n : Nat) -> SList n -> SList (max n m)
>> { insert m .zero snil = scons m zero triv snil
>> ; insert m .n (scons n k p l) = case leq n m
>>  { true  -> scons m n triv (scons n k p l)
>>  ; false -> scons n (max k m) (maxLemma k m n p (leFalse n m triv'))
>>                   (insert m k l)
>>  }
>> }
>>
>> Adding rewriting could make Agda's with more "magic" (and more
>> intuitive).  Certainly, this must have been discussed, and there are
>> reasons why it has not been implemented.
>>
>> Conor? Ulf?
>>
>> Are there theoretical obstacles (non-termination?) or is it too
>> complicated/inefficient?


- --
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.9 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iEYEARECAAYFAkpOMKEACgkQPMHaDxpUpLNPfACfb+81kPM0wR04vjLPsnn9GIbL
I+4An3EJms0F86rGOEpqONDj7iVU0+0t
=oneB
-----END PGP SIGNATURE-----