[Agda] This works in Idris by not in agda. (updating the type from the values of the constructor)

[Apostolis Xekoukoulotakis]

Andreas has a good point. It is important to keep that promise.

I case split the code in Idris by hand, but the point of types is to guide
you, thus not doing it manually.

Given that there is an easy way around it, the fact that agda rejects this
code altogether is good for pedagogical reasons.

On Sun, Dec 11, 2016 at 1:10 PM, Andreas Abel <abela at chalmers.se> wrote:

> Agda's promise is that everything that is generated by successive splits
> can be type-checked. (That this promise is not always kept is another
> story).
>
> At this point
>
>   tn : (n : ℕ) → Test (fn n) → ℕ
>   tn zero    t = {!t!}
>   tn (suc n) t = {!!}
>
> there is no way to split on t : Test 0 since it is not clear whether Tost
> is a possible case:
>
>   I'm not sure if there should be a case for the constructor Tost,
>   because I get stuck when trying to solve the following unification
>   problems (inferred index ≟ expected index):
>     fn n ≟ fn zero
>
> What should be the result of splitting on t?  A deep splitting until all
> unification constraints are satisfied??
>
> I am not sure there is a clear story behind this example, except Roman's
> advice: Be careful with function applications in the target type of your
> constructors!
>
> --Andreas
>
>
> On 11.12.2016 11:29, Jesper Cockx wrote:
>
>>     Is Agda's unifier too eager in this case?
>>
>>
>> Agda's case splitter requires all unification problems from the previous
>> case split to be solved before it can start on the next one. In other
>> words, each set of patterns must correspond to a series of consecutive
>> case splits.
>>
>> In this case, it first wants to complete the case split on the argument
>> of type "Test zero" before it continues with the case split on the
>> argument of Tost. But for this first case split Agda needs to unify zero
>> with "fn n", which fails because "fn n" doesn't reduce. It doesn't know
>> yet whether n is equal to zero or suc because that case split only comes
>> after the current one.
>>
>> In this case it would theoretically be possible to postpone the
>> unification problem and first do the second case split, which would
>> solve the problem. But in general this would be problematic as the types
>> of the constructor arguments may change as a result of the unification.
>> So a proper solution would require interleaving case splitting and
>> unification, allowing unification problems to persist over multiple case
>> splits.
>>
>> This is certainly a cool idea, but would require a nontrivial
>> engineering effort to represent this more general split-and-unify
>> problem. Does someone have an idea if this is what they do in Idris, or
>> do they have a different solution to the problem?
>>
>> Jesper
>>
>> On Sun, Dec 11, 2016 at 7:50 AM, Roman <effectfully at gmail.com
>> <mailto:effectfully at gmail.com>> wrote:
>>
>>     If you postpone unication a bit, `tn` type checks:
>>
>>     open import Relation.Binary.PropositionalEquality
>>
>>     data Test : ℕ → Set where
>>       Tist : Test zero
>>       Tostq : ∀ {m} → (n : ℕ) → m ≡ fn n → Test m
>>
>>     pattern Tost n = Tostq n refl
>>
>>     tn : (n : ℕ) → Test (fn n) → ℕ
>>     tn zero  Tist          = zero
>>     tn zero (Tost  zero)   = zero
>>     tn zero (Tost (suc n)) = zero
>>     tn (suc y) x = {!!}
>>
>>     Is Agda's unifier too eager in this case?
>>     _______________________________________________
>>     Agda mailing list
>>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>     https://lists.chalmers.se/mailman/listinfo/agda
>>     <https://lists.chalmers.se/mailman/listinfo/agda>
>>
>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161211/99d2a466/attachment.html