[Agda] Records & dependent pattern matching

[gallais at EnsL.org]

Thanks Andreas: everything works fine with a product type that is a data.
Why does NAD use a record type in the standard library? Is there a subtle thing
that I am missing?

Cheers,

--
guillaume

Ps: in my first email I was obviously talking about the *latest* version of Agda
and not the last one (hopefully there will be a couple of other ones!)


On 29 December 2010 16:21, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> Hi Guillaume,
>
> Agda 2.2.8 compiles matching against record patterns away into using
> projections.  This means that on the l.h.s., you get just a variable instead
> of a record pattern, and on the r.h.s. projections of this variable are used
> instead of the pattern components.
>
> Trying to split on pr in this situation yields an error:
>
> fail2 : ∀ {n : ℕ} (T : CTree (suc n)) → 0Tree (proj₁ T) → ℕ
> fail2 T pr = {!pr!}
>
> Cannot pattern match on constructor 0leaf, since the inferred
> indices [leaf zero] cannot be unified with the expected indices
> [proj₁ T'] for some T', n
> when checking that the expression ? has type ℕ
>
> In your situation (fail) the error handling of Agda is not very good: it
> performs the splits but then discovers it is illegal.
>
> What you can do break up the pair in the definition (as you did in
> 'success'), or you can use a product type that is a data instead of a
> record.
>
> Cheers,
> Andreas
>
> On 12/29/10 3:38 PM, gallais @ EnsL.org wrote:
>>
>> Hi all,
>>
>> I was trying to make my code (written using the 2.2.6) 2.2.8 compatible
>> and
>> I faced a problem which (I guess) comes from the way records are treated
>> in the last version of Agda.
>> Here is a simplified version of my problem:
>>
>> ===============================================================
>>
>> module failure where
>>
>> open import Data.Nat
>> open import Data.Fin
>> open import Data.Product
>>
>> -- First: define a datatype for binary trees
>> data Tree (n : ℕ) : Set where
>>   leaf : ∀ (p : Fin n) → Tree n
>>   node : ∀ (T₁ T₂ : Tree n) → Tree n
>>
>> -- Then: define 2 properties on it
>> data Comb {n : ℕ} : Tree n → Set where
>>   cleaf : ∀ (p : Fin n) → Comb (leaf p)
>>   cnode : ∀ (p : Fin n) (T : Tree n) → Comb T → Comb (node (leaf p) T)
>>
>> data 0Tree {n : ℕ} : Tree (suc n) → Set where
>>   0leaf : 0Tree (leaf zero)
>>   0node : ∀ (T₁ T₂ : Tree (suc n)) (pr₁ : 0Tree T₁) (pr₂ : 0Tree T₂) →
>> 0Tree (node T₁ T₂)
>>
>> -- Define the set of Trees that verifies the first property
>> CTree : ∀ (n : ℕ) → Set
>> CTree n = Σ (Tree n) Comb
>>
>> -- Try to define a function on Trees that are Combs&  that verifies
>> the 0Tree property
>> fail : ∀ {n : ℕ} (T : CTree (suc n)) → 0Tree (proj₁ T) → ℕ
>> fail (T , HT) pr = {!!}
>>
>> ===============================================================
>>
>> When I try to pattern match on pr, agda yields at me!:(
>>
>> Not supported: Dot patterns inside record patterns, unless
>> accompanied by data type patterns
>> when checking that the clause fail (.(leaf zero) , HT) 0leaf = ?
>> has type {n : ℕ} (T : CTree (suc n)) → 0Tree (proj₁ T) → ℕ
>>
>> I could, of course, inline everything (see success) and, then, define
>> fail as an alias
>> of success but... it's kind of ugly, isn't it?
>>
>> ===============================================================
>>
>> success : ∀ {n : ℕ} (T : Tree (suc n)) (pr₁ : Comb T) (pr₂ : 0Tree T) → ℕ
>> success T pr₁ pr₂ = {!!}
>>
>> ===============================================================
>>
>> Is there an elegant way to solve this problem? Is it normal that this
>> pattern-matching
>> isn't accepted any more?
>>
>> Cheers,
>>
>> --
>> guillaume
>>
>>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>