[Agda] Records & dependent pattern matching

[Andreas Abel]

In contrast to data, records are considered module eta-equality, e.g. x 
is identified with

   proj1 x , proj2 x

for products.  This is a nice feature, but comes with a price as you 
observed...

Cheers,
Andreas

On 12/29/10 5:49 PM, gallais @ EnsL.org wrote:
> 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
>>
>

-- 
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/