[Agda] Records with parameters depending on fields?

[Twan van Laarhoven]

You could always include the equality explicitly,

           record Snapshot Θ t i : Set where
             constructor snapshot
             field
               {Δ}         : StackType
               stack       : Stack Δ
               { Γ }       : Cxt
               environment : Env Γ
               control     : Control Γ (Θ ++ Δ) [ t ]
               isWhatever  : i ≡ (λ ss' → scon env (joinAll ss' sss))

But whether this is actually an improvement over a data type is debatable.

Twan

On 2014-06-29 20:07, Joachim Breitner wrote:
> Hi,
>
> on my way from Eugene to Portland, I finished the
> correct-according-to-the-typechecker compiler form lambda terms to the
> SECD machine. One uglifying change that I had to do was to turn the
> record
>
>          record Snapshot Θ t : Set where
>            constructor snapshot
>            field
>              {Δ}         : StackType
>              stack       : Stack Δ
>              { Γ }       : Cxt
>              environment : Env Γ
>              control     : Control Γ (Θ ++ Δ) [ t ]
>
> into a data type
>
> data Snapshot Θ t : (All El Θ → El t) → Set where
>    snapshot : ∀{Δ sss Γ} {env : Env Γ} {scon : CSem Γ (Θ ++ Δ) t} →
>               (stack : Stack Δ sss) →
>               (environment : VEnv Γ env) →
>               (control : Control Γ (Θ ++ Δ) t scon) →
>               Snapshot Θ t (λ ss' → scon env (joinAll ss' sss))
>
> because I could not see how I can make the last parameter of Snapshot an
> index that depends on the actual fields of the constructor. Is there a
> way to do that?
>
> Thanks,
> Joachim
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>