Local definitions scoping over datatype constructors

[UlfNorell]

From mech...@botik.ru on December 03, 2013 21:28:04

This is a suggestion for the language of Agda of November 2013 (which has been mentionned somewhere earlier):

to make a common let',open' possible after `where' in

              data ... where  <decls> 

Example:

data DecCommutative (A : Setoid) (∙ : Op₂ (Setoid.Carrier A)) : Set where comm : let ≈ = Setoid.≈ A open FuncProp ≈ using (Commutative) in Commutative ∙ → DecCommutative ∙_

 nonComm : let open Setoid A using (Carrier; _≈_)
           in
           (∃ \ (x y : Carrier) → ¬ x ∙ y ≈ y ∙ x) → DecCommutative _∙_

It is desirable to have a single (let ... in) after `where' instead of several ones.

Original issue: http://code.google.com/p/agda/issues/detail?id=988

[UlfNorell]

From ulf.nor...@gmail.com on December 03, 2013 13:38:17

You can achieve this using a module:

module DecCommutativeModule (A : Setoid) (∙ : Op₂ (Setoid.Carrier A)) where ≈ = Setoid.≈ A open FuncProp ≈ using (Commutative) open Setoid A using (Carrier; ≈) data DecCommutative : Set where comm : Commutative ∙_ → DecCommutative nonComm : (∃ \ (x y : Carrier) → ¬ x ∙ y ≈ y ∙ x) → DecCommutative

open DecCommutativeModule public

This is a little clunky though, so it might be worth thinking about a nicer syntax.

Summary: Local definitions scoping over datatype constructors (was: For language: open' indata' is desirable )
Labels: Type-Enhancement

[UlfNorell]

From mech...@botik.ru on December 04, 2013 00:47:15

I have forgotten of `module'. Thank you.

1) A minor question: is anonymous module possible here in
Agda - development of November 2013 ? I tried

module {α α= : Level} (A : Setoid α α=) (∙ : Op₂ (Setoid.Carrier A)) where open Setoid A using (Carrier; ≈) open FuncProp ≈_ using (Commutative)

data DecCommutative : Set (α ⊔ α=) where comm : Commutative ∙ → DecCommutative nonComm : (∃₂ \ (x y : Carrier) → ¬ (x ∙ y) ≈ (y ∙ x)) → DecCommutative

open _ public , and it is not parsed. If it is not possible, one needs to have module Dummy1, module Dummy2 ...

2) I doubt of whether introducing a module makes a program nicer than correcting the `data' syntax.

[UlfNorell]

From nils.anders.danielsson on December 04, 2013 01:14:30

"module _ where ..." means (roughly) "module Fresh where ...; open Fresh public".

[UlfNorell]

From mech...@botik.ru on December 04, 2013 02:17:15

I knew about "Fresh". But my example with "module ... open public" is not parsed. I wonder, why.

[UlfNorell]

From mech...@botik.ru on December 04, 2013 03:21:31

I am sorry, it seems that an anonymous module works without "open _ public". So, it looks all right.