[Agda] agda slow

[Ulf Norell]

There really should be a NO_ETA pragma. I made a feature request:

https://code.google.com/p/agda/issues/detail?id=1536

/ Ulf

On Tue, Jun 2, 2015 at 9:21 PM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:

> Maybe it's nicer to use if you keep the same fields:
>
> open import Data.Bool
>
> record Σ' (b : Bool) (A : Set) (B : A -> Set) : Set where
>   inductive
>   constructor _,_
>   field
>     fst : A
>     snd : if b then (B fst) else Σ' b A B
>
> Σ = Σ' true
>
> Cheers,
> Andrea
>
>
> On Tue, Jun 2, 2015 at 8:53 PM, Nils Anders Danielsson <nad at cse.gu.se>
> wrote:
> > On 2015-06-02 18:44, Andrea Vezzosi wrote:
> >>
> >> One hacky way would be to declare them coinductive, that would disable
> >> eta but also pattern matching.
> >>
> >> record Foo .. : Set where
> >>     coinductive
> >>     field
> >>        bar : ...
> >
> >
> > Another hack:
> >
> >   record Σ (A : Set) (B : A → Set) : Set where
> >     inductive
> >     field
> >       fst   : A
> >       snd   : B fst
> >       dummy : ⊥ → Σ A B
> >
> > And another one:
> >
> >   Make-Agda-believe-that-the-type-is-recursive : Set → Bool → Set
> >   Make-Agda-believe-that-the-type-is-recursive _ true  = ⊤
> >   Make-Agda-believe-that-the-type-is-recursive A false = A
> >
> >   record Σ (A : Set) (B : A → Set) : Set where
> >     inductive
> >     constructor internal-Σ-constructor
> >     field
> >       fst    : A
> >       snd    : B fst
> >       dummy₁ : Bool
> >       dummy₂ : dummy₁ ≡ true
> >       dummy₃ : Make-Agda-believe-that-the-type-is-recursive
> >                  (Σ A B) dummy₁
> >
> >   pattern _,_ x y = internal-Σ-constructor x y true refl _
> >
> > More seriously, I think there used to be an undocumented pragma that
> > turned off η-equality, but it seems to have been removed.
> >
> >> On Tue, Jun 2, 2015 at 6:03 PM, Thorsten Altenkirch
> >> <Thorsten.Altenkirch at nottingham.ac.uk> wrote:
> >>>
> >>> I was just starting to use some records to restructure some code we
> >>> are working on and the memory goes through the roof.
> >
> >
> > Can you report this on the bug tracker? Please include the two versions
> > of the code (one with lower memory consumption, and one with higher).
> >
> > --
> > /NAD
> >
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150603/0a5d62cd/attachment.html