Discussion:
[Agda] overloading operations
Sergei Meshveliani
2018-11-08 18:16:04 UTC
Permalink
Can anybody, please, explain how to arrange operation overloading
(something like classes) ?

The first example is

----------------------------------------------------------------
open import Level using (_⊔_)
open import Relation.Binary using (Setoid)

module _ {α α= β β=} (A : Setoid α α=) (B : Setoid β β=)
where
open Setoid -- {{...}}

C = Setoid.Carrier A
C' = Setoid.Carrier B

IsCongruent : (C → C') → Set _
IsCongruent f =
{x y : C} → _≈_ A x y → _≈_ B (f x) (f y) -- (I)

-- {x y : C} → x ≈ y → (f x) ≈ (f y) -- (II)

----------------------------------------------------------------


The line (I) does work.
Then I try the line (II), with un-commenting {{...}}.
And it is not type-checked.
I hoped for that it would find that the first ≈ is on C, while the
second ≈ is on C'. But it does not.

And real examples are like this:

-----------------------------------------------------------------------
module _ {α α= β β=} (G : Group α α=) (G' : Group β β=)
where
...
homomorphismPreservesInversion :
(mHomo : MonoidHomomorphism)
(let f = MonoidHomomorphism.carryMap mHomo) (x : C) →
f (x ⁻¹) ≈' (f x) ⁻¹'
homomorphismPreservesInversion
(monoidHomo ((f , f-cong) , f∙homo) f-preserves-ε) x =
begin≈'
f x' ≈'[ ≈'sym (∙ε' fx') ]
fx' ∙' ε' ≈'[ ∙'cong2 (≈'sym (x∙'x⁻¹ fx)) ]
fx' ∙' (fx ∙' fx ⁻¹') ≈'[ ≈'sym (≈'assoc fx' fx (fx ⁻¹')) ]
(fx' ∙' fx) ∙' fx ⁻¹' ≈'[ ∙'cong1 (≈'sym (f∙homo x' x)) ]
f (x' ∙ x) ∙' fx ⁻¹' ≈'[ ∙'cong1 (f-cong (x⁻¹∙x x)) ]
f ε ∙' fx ⁻¹' ≈'[ ∙'cong1 f-preserves-ε ]
ε' ∙' fx ⁻¹' ≈'[ ε'∙ (fx ⁻¹') ]
(f x) ⁻¹'
end≈'
where
x' = x ⁻¹; fx = f x; fx' = f x'
----------------------------------------------------------------------

Here the carriers of G and G' are C and C',
≈ is on C, ≈' is on C' (by renaming),
_∙_ on C, _∙'_ on C',
ε is of G, ε' of G',
_⁻¹ is of G, _⁻¹' of G',
and so on.

It is desirable to make the code more readable by canceling some of the
above renaming. For example, to replace ε' with ε and _∙'_ with _∙_.
Is it possible to do this by using something like
open Group {{...}}
?

Thanks,

------
Sergei
James Wood
2018-11-09 17:28:55 UTC
Permalink
Agda doesn't do overloading for anything other than constructors, but
there are still tricks you can use. One I use a lot is making a local
module definition just to make a quick namespace, and then use dot
notation to access the contents of that module. In your example, it
would look like this:

module A = Setoid A
module B = Setoid B

IsCongruent : (A.Carrier → B.Carrier) → Set _
IsCongruent f = {x y} → x A.≈ y → (f x) B.≈ (f y)

Perhaps not ideal, but I've found it okay.

James
Post by Sergei Meshveliani
Can anybody, please, explain how to arrange operation overloading
(something like classes) ?
The first example is
----------------------------------------------------------------
open import Level using (_⊔_)
open import Relation.Binary using (Setoid)
module _ {α α= β β=} (A : Setoid α α=) (B : Setoid β β=)
where
open Setoid -- {{...}}
C = Setoid.Carrier A
C' = Setoid.Carrier B
IsCongruent : (C → C') → Set _
IsCongruent f =
{x y : C} → _≈_ A x y → _≈_ B (f x) (f y) -- (I)
-- {x y : C} → x ≈ y → (f x) ≈ (f y) -- (II)
----------------------------------------------------------------
The line (I) does work.
Then I try the line (II), with un-commenting {{...}}.
And it is not type-checked.
I hoped for that it would find that the first ≈ is on C, while the
second ≈ is on C'. But it does not.
-----------------------------------------------------------------------
module _ {α α= β β=} (G : Group α α=) (G' : Group β β=)
where
...
(mHomo : MonoidHomomorphism)
(let f = MonoidHomomorphism.carryMap mHomo) (x : C) →
f (x ⁻¹) ≈' (f x) ⁻¹'
homomorphismPreservesInversion
(monoidHomo ((f , f-cong) , f∙homo) f-preserves-ε) x =
begin≈'
f x' ≈'[ ≈'sym (∙ε' fx') ]
fx' ∙' ε' ≈'[ ∙'cong2 (≈'sym (x∙'x⁻¹ fx)) ]
fx' ∙' (fx ∙' fx ⁻¹') ≈'[ ≈'sym (≈'assoc fx' fx (fx ⁻¹')) ]
(fx' ∙' fx) ∙' fx ⁻¹' ≈'[ ∙'cong1 (≈'sym (f∙homo x' x)) ]
f (x' ∙ x) ∙' fx ⁻¹' ≈'[ ∙'cong1 (f-cong (x⁻¹∙x x)) ]
f ε ∙' fx ⁻¹' ≈'[ ∙'cong1 f-preserves-ε ]
ε' ∙' fx ⁻¹' ≈'[ ε'∙ (fx ⁻¹') ]
(f x) ⁻¹'
end≈'
where
x' = x ⁻¹; fx = f x; fx' = f x'
----------------------------------------------------------------------
Here the carriers of G and G' are C and C',
≈ is on C, ≈' is on C' (by renaming),
_∙_ on C, _∙'_ on C',
ε is of G, ε' of G',
_⁻¹ is of G, _⁻¹' of G',
and so on.
It is desirable to make the code more readable by canceling some of the
above renaming. For example, to replace ε' with ε and _∙'_ with _∙_.
Is it possible to do this by using something like
open Group {{...}}
?
Thanks,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
--
James Wood,
Department of Computer and Information Sciences,
University of Strathclyde.
The University of Strathclyde is a charitable body, registered in
Scotland, with registration number SC015263.
Sergei Meshveliani
2018-11-09 18:41:16 UTC
Permalink
Post by James Wood
Agda doesn't do overloading for anything other than constructors, but
there are still tricks you can use. One I use a lot is making a local
module definition just to make a quick namespace, and then use dot
notation to access the contents of that module. In your example, it
module A = Setoid A
module B = Setoid B
IsCongruent : (A.Carrier → B.Carrier) → Set _
IsCongruent f = {x y} → x A.≈ y → (f x) B.≈ (f y)
Perhaps not ideal, but I've found it okay.
Thank you.
Currently I also use such in my example: P'.∙ε, P'.x∙x⁻¹, P'.∙cong2.

But it is essentially worse than ∙ε, x∙x⁻¹, ∙cong2.

I also have a renaming of ≈', which looks better than A.≈,
Also ≈ can be renamed to ≈A, which looks better than A.≈.
And all them are worse than ≈.

--
SM
Post by James Wood
Post by Sergei Meshveliani
Can anybody, please, explain how to arrange operation overloading
(something like classes) ?
The first example is
----------------------------------------------------------------
open import Level using (_⊔_)
open import Relation.Binary using (Setoid)
module _ {α α= β β=} (A : Setoid α α=) (B : Setoid β β=)
where
open Setoid -- {{...}}
C = Setoid.Carrier A
C' = Setoid.Carrier B
IsCongruent : (C → C') → Set _
IsCongruent f =
{x y : C} → _≈_ A x y → _≈_ B (f x) (f y) -- (I)
-- {x y : C} → x ≈ y → (f x) ≈ (f y) -- (II)
----------------------------------------------------------------
The line (I) does work.
Then I try the line (II), with un-commenting {{...}}.
And it is not type-checked.
I hoped for that it would find that the first ≈ is on C, while the
second ≈ is on C'. But it does not.
-----------------------------------------------------------------------
module _ {α α= β β=} (G : Group α α=) (G' : Group β β=)
where
...
(mHomo : MonoidHomomorphism)
(let f = MonoidHomomorphism.carryMap mHomo) (x : C) →
f (x ⁻¹) ≈' (f x) ⁻¹'
homomorphismPreservesInversion
(monoidHomo ((f , f-cong) , f∙homo) f-preserves-ε) x =
begin≈'
f x' ≈'[ ≈'sym (∙ε' fx') ]
fx' ∙' ε' ≈'[ ∙'cong2 (≈'sym (x∙'x⁻¹ fx)) ]
fx' ∙' (fx ∙' fx ⁻¹') ≈'[ ≈'sym (≈'assoc fx' fx (fx ⁻¹')) ]
(fx' ∙' fx) ∙' fx ⁻¹' ≈'[ ∙'cong1 (≈'sym (f∙homo x' x)) ]
f (x' ∙ x) ∙' fx ⁻¹' ≈'[ ∙'cong1 (f-cong (x⁻¹∙x x)) ]
f ε ∙' fx ⁻¹' ≈'[ ∙'cong1 f-preserves-ε ]
ε' ∙' fx ⁻¹' ≈'[ ε'∙ (fx ⁻¹') ]
(f x) ⁻¹'
end≈'
where
x' = x ⁻¹; fx = f x; fx' = f x'
----------------------------------------------------------------------
Here the carriers of G and G' are C and C',
≈ is on C, ≈' is on C' (by renaming),
_∙_ on C, _∙'_ on C',
ε is of G, ε' of G',
_⁻¹ is of G, _⁻¹' of G',
and so on.
It is desirable to make the code more readable by canceling some of the
above renaming. For example, to replace ε' with ε and _∙'_ with _∙_.
Is it possible to do this by using something like
open Group {{...}}
?
Thanks,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Martín Hötzel Escardó
2018-11-09 19:49:08 UTC
Permalink
Hi Sergei, I have a situation very similar to yours.

An ordinal is a type equipped with a relation _≺_ and a justification
that it is a well-order. Moreover, this order has an automatically
derived partial order _≼_.

If α is an ordinal, then I write ⟨ α ⟩ for the underlying type of α and
x ≺⟨ α ⟩ y and x ≼⟨ α ⟩ y for its underlying orders (given and derived).

The notation ⟨_⟩ for the underlying type is defined directly, just as a
projection.

The notations for the given and derived orders are given by "syntax"
declarations,

syntax underlying-order α x y = x ≺⟨ α ⟩ y
syntax underlying-porder α x y = x ≼⟨ α ⟩ y

where the underlying things are again projections.

I found that this worked quite well (although it would have been much
better if Agda could infer the "subscript" α for the orders, given that
x and y are known to live in the type ⟨ α ⟩).

Here are some examples from
http://www.cs.bham.ac.uk/~mhe/agda-new/OrdinalOfOrdinals.html

is-order-preserving
is-monotone
is-order-reflecting
is-order-embedding
is-order-equiv
is-initial-segment
is-simulation
: (α : Ordinal U) (β : Ordinal V) → (⟨ α ⟩ → ⟨ β ⟩) → U ⊔ V ̇

is-order-preserving α β f = (x y : ⟨ α ⟩) → x ≺⟨ α ⟩ y → f x ≺⟨ β ⟩ f y

is-monotone α β f = (x y : ⟨ α ⟩) → x ≼⟨ α ⟩ y → f x ≼⟨ β ⟩ f y

is-order-reflecting α β f = (x y : ⟨ α ⟩) → f x ≺⟨ β ⟩ f y → x ≺⟨ α ⟩ y

...

(Warning: I use U,V,W for type universes rather than "Set i" notation,
but this is another story. Additionally, U,V,W are "variables", a newly
introduced feature which is available in the development version only.)

I presume you could define a type "Setoid U" of setoids in the universe
U with very much the same underlying-type and underlying-equivalence
notation.

Martin
Post by Sergei Meshveliani
Post by James Wood
Agda doesn't do overloading for anything other than constructors, but
there are still tricks you can use. One I use a lot is making a local
module definition just to make a quick namespace, and then use dot
notation to access the contents of that module. In your example, it
module A = Setoid A
module B = Setoid B
IsCongruent : (A.Carrier → B.Carrier) → Set _
IsCongruent f = {x y} → x A.≈ y → (f x) B.≈ (f y)
Perhaps not ideal, but I've found it okay.
Thank you.
Currently I also use such in my example: P'.∙ε, P'.x∙x⁻¹, P'.∙cong2.
But it is essentially worse than ∙ε, x∙x⁻¹, ∙cong2.
I also have a renaming of ≈', which looks better than A.≈,
Also ≈ can be renamed to ≈A, which looks better than A.≈.
And all them are worse than ≈.
--
SM
Post by James Wood
Post by Sergei Meshveliani
Can anybody, please, explain how to arrange operation overloading
(something like classes) ?
The first example is
----------------------------------------------------------------
open import Level using (_⊔_)
open import Relation.Binary using (Setoid)
module _ {α α= β β=} (A : Setoid α α=) (B : Setoid β β=)
where
open Setoid -- {{...}}
C = Setoid.Carrier A
C' = Setoid.Carrier B
IsCongruent : (C → C') → Set _
IsCongruent f =
{x y : C} → _≈_ A x y → _≈_ B (f x) (f y) -- (I)
-- {x y : C} → x ≈ y → (f x) ≈ (f y) -- (II)
----------------------------------------------------------------
The line (I) does work.
Then I try the line (II), with un-commenting {{...}}.
And it is not type-checked.
I hoped for that it would find that the first ≈ is on C, while the
second ≈ is on C'. But it does not.
-----------------------------------------------------------------------
module _ {α α= β β=} (G : Group α α=) (G' : Group β β=)
where
...
(mHomo : MonoidHomomorphism)
(let f = MonoidHomomorphism.carryMap mHomo) (x : C) →
f (x ⁻¹) ≈' (f x) ⁻¹'
homomorphismPreservesInversion
(monoidHomo ((f , f-cong) , f∙homo) f-preserves-ε) x =
begin≈'
f x' ≈'[ ≈'sym (∙ε' fx') ]
fx' ∙' ε' ≈'[ ∙'cong2 (≈'sym (x∙'x⁻¹ fx)) ]
fx' ∙' (fx ∙' fx ⁻¹') ≈'[ ≈'sym (≈'assoc fx' fx (fx ⁻¹')) ]
(fx' ∙' fx) ∙' fx ⁻¹' ≈'[ ∙'cong1 (≈'sym (f∙homo x' x)) ]
f (x' ∙ x) ∙' fx ⁻¹' ≈'[ ∙'cong1 (f-cong (x⁻¹∙x x)) ]
f ε ∙' fx ⁻¹' ≈'[ ∙'cong1 f-preserves-ε ]
ε' ∙' fx ⁻¹' ≈'[ ε'∙ (fx ⁻¹') ]
(f x) ⁻¹'
end≈'
where
x' = x ⁻¹; fx = f x; fx' = f x'
----------------------------------------------------------------------
Here the carriers of G and G' are C and C',
≈ is on C, ≈' is on C' (by renaming),
_∙_ on C, _∙'_ on C',
ε is of G, ε' of G',
_⁻¹ is of G, _⁻¹' of G',
and so on.
It is desirable to make the code more readable by canceling some of the
above renaming. For example, to replace ε' with ε and _∙'_ with _∙_.
Is it possible to do this by using something like
open Group {{...}}
?
Thanks,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
--
http://www.cs.bham.ac.uk/~mhe
Guillaume Brunerie
2018-11-09 20:28:26 UTC
Permalink
Hi Martin, have you tried with instance arguments?
Here is a self-contained example, based on your code, showing how to get

is-order-preserving α β f = (x y : ⟨ α ⟩) → x ≺ y → f x ≺ f y

The main changes are that I define Ordinal using a special Σ-type
where the second field is an instance field, and then _≺_ takes the
ordinal structure as an instance argument.


open import Agda.Primitive public
using (_⊔_)
renaming (lzero to U₀
; lsuc to _⁺
; Level to Universe
; Setω to Uω
)

variable
U V W U' V' W' : Universe

_̇ : (U : Universe) → _
U ̇ = Set U

record Σ {U V} {X : U ̇} (Y : X → V ̇) : (U ⊔ V) ̇ where
constructor _,_
field
pr₁ : X
pr₂ : Y pr₁

open Σ public

infixr 4 _,_

postulate
is-well-order : {U V : Universe}
{X : U ̇}
(_<_ : X → X → V ̇) → (U ⊔ V) ̇

OrdinalStructure : U ̇ → U ⁺ ̇
OrdinalStructure {U} X = Σ \(_<_ : X → X → U ̇) → is-well-order _<_

{- A Σ-type where the second field is an instance argument -}
record Σ⦃⦄ {U V} {X : U ̇} (Y : X → V ̇) : (U ⊔ V) ̇ where
constructor σ
field
pr₁ : X
{{pr₂}} : Y pr₁

Ordinal : ∀ U → U ⁺ ̇
Ordinal U = Σ⦃⦄ \(X : U ̇) → OrdinalStructure X

⟨_⟩ : Ordinal U → U ̇
⟨ σ X ⟩ = X

_≺_ : {X : U ̇} {{_ : OrdinalStructure X}} → X → X → U ̇
_≺_ {{_<_ , o}} = _<_

is-order-preserving : (α : Ordinal U) (β : Ordinal V) → (⟨ α ⟩ → ⟨ β
⟩) → (U ⊔ V) ̇
is-order-preserving α β f = (x y : ⟨ α ⟩) → x ≺ y → f x ≺ f y
Den fre 9 nov. 2018 kl 20:49 skrev Martín Hötzel Escardó
Post by Martín Hötzel Escardó
Hi Sergei, I have a situation very similar to yours.
An ordinal is a type equipped with a relation _≺_ and a justification
that it is a well-order. Moreover, this order has an automatically
derived partial order _≼_.
If α is an ordinal, then I write ⟨ α ⟩ for the underlying type of α and
x ≺⟨ α ⟩ y and x ≼⟨ α ⟩ y for its underlying orders (given and derived).
The notation ⟨_⟩ for the underlying type is defined directly, just as a
projection.
The notations for the given and derived orders are given by "syntax"
declarations,
syntax underlying-order α x y = x ≺⟨ α ⟩ y
syntax underlying-porder α x y = x ≼⟨ α ⟩ y
where the underlying things are again projections.
I found that this worked quite well (although it would have been much
better if Agda could infer the "subscript" α for the orders, given that
x and y are known to live in the type ⟨ α ⟩).
Here are some examples from
http://www.cs.bham.ac.uk/~mhe/agda-new/OrdinalOfOrdinals.html
is-order-preserving
is-monotone
is-order-reflecting
is-order-embedding
is-order-equiv
is-initial-segment
is-simulation
: (α : Ordinal U) (β : Ordinal V) → (⟨ α ⟩ → ⟨ β ⟩) → U ⊔ V ̇
is-order-preserving α β f = (x y : ⟨ α ⟩) → x ≺⟨ α ⟩ y → f x ≺⟨ β ⟩ f y
is-monotone α β f = (x y : ⟨ α ⟩) → x ≼⟨ α ⟩ y → f x ≼⟨ β ⟩ f y
is-order-reflecting α β f = (x y : ⟨ α ⟩) → f x ≺⟨ β ⟩ f y → x ≺⟨ α ⟩ y
...
(Warning: I use U,V,W for type universes rather than "Set i" notation,
but this is another story. Additionally, U,V,W are "variables", a newly
introduced feature which is available in the development version only.)
I presume you could define a type "Setoid U" of setoids in the universe
U with very much the same underlying-type and underlying-equivalence
notation.
Martin
Post by Sergei Meshveliani
Post by James Wood
Agda doesn't do overloading for anything other than constructors, but
there are still tricks you can use. One I use a lot is making a local
module definition just to make a quick namespace, and then use dot
notation to access the contents of that module. In your example, it
module A = Setoid A
module B = Setoid B
IsCongruent : (A.Carrier → B.Carrier) → Set _
IsCongruent f = {x y} → x A.≈ y → (f x) B.≈ (f y)
Perhaps not ideal, but I've found it okay.
Thank you.
Currently I also use such in my example: P'.∙ε, P'.x∙x⁻¹, P'.∙cong2.
But it is essentially worse than ∙ε, x∙x⁻¹, ∙cong2.
I also have a renaming of ≈', which looks better than A.≈,
Also ≈ can be renamed to ≈A, which looks better than A.≈.
And all them are worse than ≈.
--
SM
Post by James Wood
Post by Sergei Meshveliani
Can anybody, please, explain how to arrange operation overloading
(something like classes) ?
The first example is
----------------------------------------------------------------
open import Level using (_⊔_)
open import Relation.Binary using (Setoid)
module _ {α α= β β=} (A : Setoid α α=) (B : Setoid β β=)
where
open Setoid -- {{...}}
C = Setoid.Carrier A
C' = Setoid.Carrier B
IsCongruent : (C → C') → Set _
IsCongruent f =
{x y : C} → _≈_ A x y → _≈_ B (f x) (f y) -- (I)
-- {x y : C} → x ≈ y → (f x) ≈ (f y) -- (II)
----------------------------------------------------------------
The line (I) does work.
Then I try the line (II), with un-commenting {{...}}.
And it is not type-checked.
I hoped for that it would find that the first ≈ is on C, while the
second ≈ is on C'. But it does not.
-----------------------------------------------------------------------
module _ {α α= β β=} (G : Group α α=) (G' : Group β β=)
where
...
(mHomo : MonoidHomomorphism)
(let f = MonoidHomomorphism.carryMap mHomo) (x : C) →
f (x ⁻¹) ≈' (f x) ⁻¹'
homomorphismPreservesInversion
(monoidHomo ((f , f-cong) , f∙homo) f-preserves-ε) x =
begin≈'
f x' ≈'[ ≈'sym (∙ε' fx') ]
fx' ∙' ε' ≈'[ ∙'cong2 (≈'sym (x∙'x⁻¹ fx)) ]
fx' ∙' (fx ∙' fx ⁻¹') ≈'[ ≈'sym (≈'assoc fx' fx (fx ⁻¹')) ]
(fx' ∙' fx) ∙' fx ⁻¹' ≈'[ ∙'cong1 (≈'sym (f∙homo x' x)) ]
f (x' ∙ x) ∙' fx ⁻¹' ≈'[ ∙'cong1 (f-cong (x⁻¹∙x x)) ]
f ε ∙' fx ⁻¹' ≈'[ ∙'cong1 f-preserves-ε ]
ε' ∙' fx ⁻¹' ≈'[ ε'∙ (fx ⁻¹') ]
(f x) ⁻¹'
end≈'
where
x' = x ⁻¹; fx = f x; fx' = f x'
----------------------------------------------------------------------
Here the carriers of G and G' are C and C',
≈ is on C, ≈' is on C' (by renaming),
_∙_ on C, _∙'_ on C',
ε is of G, ε' of G',
_⁻¹ is of G, _⁻¹' of G',
and so on.
It is desirable to make the code more readable by canceling some of the
above renaming. For example, to replace ε' with ε and _∙'_ with _∙_.
Is it possible to do this by using something like
open Group {{...}}
?
Thanks,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
--
http://www.cs.bham.ac.uk/~mhe
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Martin Escardo
2018-11-09 21:51:55 UTC
Permalink
Post by Guillaume Brunerie
Hi Martin, have you tried with instance arguments?
Thanks! I will try your suggestion below and if it works well with the
whole development (27k lines, 100 files) I may adopt it.

Martin
Post by Guillaume Brunerie
Here is a self-contained example, based on your code, showing how to get
is-order-preserving α β f = (x y : ⟨ α ⟩) → x ≺ y → f x ≺ f y
The main changes are that I define Ordinal using a special Σ-type
where the second field is an instance field, and then _≺_ takes the
ordinal structure as an instance argument.
open import Agda.Primitive public
using (_⊔_)
renaming (lzero to U₀
; lsuc to _⁺
; Level to Universe
; Setω to Uω
)
variable
U V W U' V' W' : Universe
_̇ : (U : Universe) → _
U ̇ = Set U
record Σ {U V} {X : U ̇} (Y : X → V ̇) : (U ⊔ V) ̇ where
constructor _,_
field
pr₁ : X
pr₂ : Y pr₁
open Σ public
infixr 4 _,_
postulate
is-well-order : {U V : Universe}
{X : U ̇}
(_<_ : X → X → V ̇) → (U ⊔ V) ̇
OrdinalStructure : U ̇ → U ⁺ ̇
OrdinalStructure {U} X = Σ \(_<_ : X → X → U ̇) → is-well-order _<_
{- A Σ-type where the second field is an instance argument -}
record Σ⦃⦄ {U V} {X : U ̇} (Y : X → V ̇) : (U ⊔ V) ̇ where
constructor σ
field
pr₁ : X
{{pr₂}} : Y pr₁
Ordinal : ∀ U → U ⁺ ̇
Ordinal U = Σ⦃⦄ \(X : U ̇) → OrdinalStructure X
⟨_⟩ : Ordinal U → U ̇
⟨ σ X ⟩ = X
_≺_ : {X : U ̇} {{_ : OrdinalStructure X}} → X → X → U ̇
_≺_ {{_<_ , o}} = _<_
is-order-preserving : (α : Ordinal U) (β : Ordinal V) → (⟨ α ⟩ → ⟨ β
⟩) → (U ⊔ V) ̇
is-order-preserving α β f = (x y : ⟨ α ⟩) → x ≺ y → f x ≺ f y
Den fre 9 nov. 2018 kl 20:49 skrev Martín Hötzel Escardó
Post by Martín Hötzel Escardó
Hi Sergei, I have a situation very similar to yours.
An ordinal is a type equipped with a relation _≺_ and a justification
that it is a well-order. Moreover, this order has an automatically
derived partial order _≼_.
If α is an ordinal, then I write ⟨ α ⟩ for the underlying type of α and
x ≺⟨ α ⟩ y and x ≼⟨ α ⟩ y for its underlying orders (given and derived).
The notation ⟨_⟩ for the underlying type is defined directly, just as a
projection.
The notations for the given and derived orders are given by "syntax"
declarations,
syntax underlying-order α x y = x ≺⟨ α ⟩ y
syntax underlying-porder α x y = x ≼⟨ α ⟩ y
where the underlying things are again projections.
I found that this worked quite well (although it would have been much
better if Agda could infer the "subscript" α for the orders, given that
x and y are known to live in the type ⟨ α ⟩).
Here are some examples from
http://www.cs.bham.ac.uk/~mhe/agda-new/OrdinalOfOrdinals.html
is-order-preserving
is-monotone
is-order-reflecting
is-order-embedding
is-order-equiv
is-initial-segment
is-simulation
: (α : Ordinal U) (β : Ordinal V) → (⟨ α ⟩ → ⟨ β ⟩) → U ⊔ V ̇
is-order-preserving α β f = (x y : ⟨ α ⟩) → x ≺⟨ α ⟩ y → f x ≺⟨ β ⟩ f y
is-monotone α β f = (x y : ⟨ α ⟩) → x ≼⟨ α ⟩ y → f x ≼⟨ β ⟩ f y
is-order-reflecting α β f = (x y : ⟨ α ⟩) → f x ≺⟨ β ⟩ f y → x ≺⟨ α ⟩ y
...
(Warning: I use U,V,W for type universes rather than "Set i" notation,
but this is another story. Additionally, U,V,W are "variables", a newly
introduced feature which is available in the development version only.)
I presume you could define a type "Setoid U" of setoids in the universe
U with very much the same underlying-type and underlying-equivalence
notation.
Martin
Post by Sergei Meshveliani
Post by James Wood
Agda doesn't do overloading for anything other than constructors, but
there are still tricks you can use. One I use a lot is making a local
module definition just to make a quick namespace, and then use dot
notation to access the contents of that module. In your example, it
module A = Setoid A
module B = Setoid B
IsCongruent : (A.Carrier → B.Carrier) → Set _
IsCongruent f = {x y} → x A.≈ y → (f x) B.≈ (f y)
Perhaps not ideal, but I've found it okay.
Thank you.
Currently I also use such in my example: P'.∙ε, P'.x∙x⁻¹, P'.∙cong2.
But it is essentially worse than ∙ε, x∙x⁻¹, ∙cong2.
I also have a renaming of ≈', which looks better than A.≈,
Also ≈ can be renamed to ≈A, which looks better than A.≈.
And all them are worse than ≈.
--
SM
Post by James Wood
Post by Sergei Meshveliani
Can anybody, please, explain how to arrange operation overloading
(something like classes) ?
The first example is
----------------------------------------------------------------
open import Level using (_⊔_)
open import Relation.Binary using (Setoid)
module _ {α α= β β=} (A : Setoid α α=) (B : Setoid β β=)
where
open Setoid -- {{...}}
C = Setoid.Carrier A
C' = Setoid.Carrier B
IsCongruent : (C → C') → Set _
IsCongruent f =
{x y : C} → _≈_ A x y → _≈_ B (f x) (f y) -- (I)
-- {x y : C} → x ≈ y → (f x) ≈ (f y) -- (II)
----------------------------------------------------------------
The line (I) does work.
Then I try the line (II), with un-commenting {{...}}.
And it is not type-checked.
I hoped for that it would find that the first ≈ is on C, while the
second ≈ is on C'. But it does not.
-----------------------------------------------------------------------
module _ {α α= β β=} (G : Group α α=) (G' : Group β β=)
where
...
(mHomo : MonoidHomomorphism)
(let f = MonoidHomomorphism.carryMap mHomo) (x : C) →
f (x ⁻¹) ≈' (f x) ⁻¹'
homomorphismPreservesInversion
(monoidHomo ((f , f-cong) , f∙homo) f-preserves-ε) x =
begin≈'
f x' ≈'[ ≈'sym (∙ε' fx') ]
fx' ∙' ε' ≈'[ ∙'cong2 (≈'sym (x∙'x⁻¹ fx)) ]
fx' ∙' (fx ∙' fx ⁻¹') ≈'[ ≈'sym (≈'assoc fx' fx (fx ⁻¹')) ]
(fx' ∙' fx) ∙' fx ⁻¹' ≈'[ ∙'cong1 (≈'sym (f∙homo x' x)) ]
f (x' ∙ x) ∙' fx ⁻¹' ≈'[ ∙'cong1 (f-cong (x⁻¹∙x x)) ]
f ε ∙' fx ⁻¹' ≈'[ ∙'cong1 f-preserves-ε ]
ε' ∙' fx ⁻¹' ≈'[ ε'∙ (fx ⁻¹') ]
(f x) ⁻¹'
end≈'
where
x' = x ⁻¹; fx = f x; fx' = f x'
----------------------------------------------------------------------
Here the carriers of G and G' are C and C',
≈ is on C, ≈' is on C' (by renaming),
_∙_ on C, _∙'_ on C',
ε is of G, ε' of G',
_⁻¹ is of G, _⁻¹' of G',
and so on.
It is desirable to make the code more readable by canceling some of the
above renaming. For example, to replace ε' with ε and _∙'_ with _∙_.
Is it possible to do this by using something like
open Group {{...}}
?
Thanks,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
--
http://www.cs.bham.ac.uk/~mhe
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe
Sergei Meshveliani
2018-11-10 12:22:27 UTC
Permalink
Post by Martín Hötzel Escardó
Hi Sergei, I have a situation very similar to yours.
An ordinal is a type equipped with a relation _≺_ and a justification
that it is a well-order. Moreover, this order has an automatically
derived partial order _≼_.
If α is an ordinal, then I write ⟨ α ⟩ for the underlying type of α and
x ≺⟨ α ⟩ y and x ≼⟨ α ⟩ y for its underlying orders (given and derived).
The notation ⟨_⟩ for the underlying type is defined directly, just as a
projection.
The notations for the given and derived orders are given by "syntax"
declarations,
syntax underlying-order α x y = x ≺⟨ α ⟩ y
syntax underlying-porder α x y = x ≼⟨ α ⟩ y
where the underlying things are again projections.
I found that this worked quite well (although it would have been much
better if Agda could infer the "subscript" α for the orders, given that
x and y are known to live in the type ⟨ α ⟩).
Here are some examples from
http://www.cs.bham.ac.uk/~mhe/agda-new/OrdinalOfOrdinals.html
is-order-preserving
is-monotone
is-order-reflecting
is-order-embedding
is-order-equiv
is-initial-segment
is-simulation
: (α : Ordinal U) (β : Ordinal V) → (⟨ α ⟩ → ⟨ β ⟩) → U ⊔ V ̇
is-order-preserving α β f = (x y : ⟨ α ⟩) → x ≺⟨ α ⟩ y → f x ≺⟨ β ⟩ f y
is-monotone α β f = (x y : ⟨ α ⟩) → x ≼⟨ α ⟩ y → f x ≼⟨ β ⟩ f y
is-order-reflecting α β f = (x y : ⟨ α ⟩) → f x ≺⟨ β ⟩ f y → x ≺⟨ α ⟩ y
...
(Warning: I use U,V,W for type universes rather than "Set i" notation,
but this is another story. Additionally, U,V,W are "variables", a newly
introduced feature which is available in the development version only.)
I presume you could define a type "Setoid U" of setoids in the universe
U with very much the same underlying-type and underlying-equivalence
notation.
In my first reply I have probably confused things about universes.

Now I try once more to understand the idea.
Let us look at the result of this technique. Your demonstration shows
the usage of this technique:

is-order-preserving α β f =
(x y : ⟨ α ⟩) → x ≺⟨ α ⟩ y → f x ≺⟨ β ⟩ f y

But the denotation ≺⟨ α ⟩ and ≺⟨ β ⟩ is not any better than
≺α and ≺β which uses renaming.


Am I missing something?


The goal is overloading. That is this signature needs to be

(x y : ⟨ α ⟩) → x ≺ y → f x ≺ f y (I)

According to the type of f, the first occurrence of ≺ needs to be
recognized by the type checker as on α and the second occurrence of ≺
needs to be recognized as on β.

Agda tends to be considered as an extension of Haskell.
But Haskell allows such overloading (to a certain extent) through the
mechanism of classes and instances. For example, (<), (+), (*).
are declared in Haskell library as certain class members, and are
overloaded like in (I).
I recall difficulties with constant operations and with overlapping
instances, but classes work there, to a certain extent.

Probably, the only remaining hope in Agda is for instance arguments,
something about the ``open ... {{...}}'' denotation.
I try it for Setoid._≈_, Semigroup._∙_, and it does not work.

Guillaume writes that to do this with respect to Standard library
operations, one needs to reorganize Standard library, a bit: to make
Carrier to be an argument to Setoid, and so on.
This means rewriting things in a certain programming style.

Regards,

------
Sergei
Post by Martín Hötzel Escardó
Post by Martín Hötzel Escardó
Post by Sergei Meshveliani
Post by James Wood
Agda doesn't do overloading for anything other than constructors, but
there are still tricks you can use. One I use a lot is making a local
module definition just to make a quick namespace, and then use dot
notation to access the contents of that module. In your example, it
module A = Setoid A
module B = Setoid B
IsCongruent : (A.Carrier → B.Carrier) → Set _
IsCongruent f = {x y} → x A.≈ y → (f x) B.≈ (f y)
Perhaps not ideal, but I've found it okay.
Thank you.
Currently I also use such in my example: P'.∙ε, P'.x∙x⁻¹, P'.∙cong2.
But it is essentially worse than ∙ε, x∙x⁻¹, ∙cong2.
I also have a renaming of ≈', which looks better than A.≈,
Also ≈ can be renamed to ≈A, which looks better than A.≈.
And all them are worse than ≈.
--
SM
Post by James Wood
Post by Sergei Meshveliani
Can anybody, please, explain how to arrange operation overloading
(something like classes) ?
The first example is
----------------------------------------------------------------
open import Level using (_⊔_)
open import Relation.Binary using (Setoid)
module _ {α α= β β=} (A : Setoid α α=) (B : Setoid β β=)
where
open Setoid -- {{...}}
C = Setoid.Carrier A
C' = Setoid.Carrier B
IsCongruent : (C → C') → Set _
IsCongruent f =
{x y : C} → _≈_ A x y → _≈_ B (f x) (f y) -- (I)
-- {x y : C} → x ≈ y → (f x) ≈ (f y) -- (II)
----------------------------------------------------------------
The line (I) does work.
Then I try the line (II), with un-commenting {{...}}.
And it is not type-checked.
I hoped for that it would find that the first ≈ is on C, while the
second ≈ is on C'. But it does not.
-----------------------------------------------------------------------
module _ {α α= β β=} (G : Group α α=) (G' : Group β β=)
where
...
(mHomo : MonoidHomomorphism)
(let f = MonoidHomomorphism.carryMap mHomo) (x : C) →
f (x ⁻¹) ≈' (f x) ⁻¹'
homomorphismPreservesInversion
(monoidHomo ((f , f-cong) , f∙homo) f-preserves-ε) x =
begin≈'
f x' ≈'[ ≈'sym (∙ε' fx') ]
fx' ∙' ε' ≈'[ ∙'cong2 (≈'sym (x∙'x⁻¹ fx)) ]
fx' ∙' (fx ∙' fx ⁻¹') ≈'[ ≈'sym (≈'assoc fx' fx (fx ⁻¹')) ]
(fx' ∙' fx) ∙' fx ⁻¹' ≈'[ ∙'cong1 (≈'sym (f∙homo x' x)) ]
f (x' ∙ x) ∙' fx ⁻¹' ≈'[ ∙'cong1 (f-cong (x⁻¹∙x x)) ]
f ε ∙' fx ⁻¹' ≈'[ ∙'cong1 f-preserves-ε ]
ε' ∙' fx ⁻¹' ≈'[ ε'∙ (fx ⁻¹') ]
(f x) ⁻¹'
end≈'
where
x' = x ⁻¹; fx = f x; fx' = f x'
----------------------------------------------------------------------
Here the carriers of G and G' are C and C',
≈ is on C, ≈' is on C' (by renaming),
_∙_ on C, _∙'_ on C',
ε is of G, ε' of G',
_⁻¹ is of G, _⁻¹' of G',
and so on.
It is desirable to make the code more readable by canceling some of the
above renaming. For example, to replace ε' with ε and _∙'_ with _∙_.
Is it possible to do this by using something like
open Group {{...}}
?
Thanks,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
--
http://www.cs.bham.ac.uk/~mhe
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Guillaume Allais
2018-11-11 11:42:49 UTC
Permalink
Hi Sergei,

Note that you don't the stdlib to change to be able to use Guillaume's
approach: you can add a layer on top of the stdlib giving a definition
of Semigroup exposing the Carrier and add a generic instance converting
from the stdlib's style to that new style. Self-contained example:

===================================================================
open import Level
open import Algebra
open import Algebra.Structures
open import Algebra.FunctionProperties.Core
open import Relation.Binary

record OverloadedSemigroup {c} (Carrier : Set c) ℓ : Set (c ⊔ suc ℓ) where
infixl 7 _∙_
infix 4 _≈_
field
_≈_ : Rel Carrier ℓ
_∙_ : Op₂ Carrier
isSemigroup : IsSemigroup _≈_ _∙_

instance
OS : ∀ {c ℓ} {{S : Semigroup c ℓ}} →
OverloadedSemigroup (Semigroup.Carrier S) ℓ
OS {{S}} = record { Semigroup S }

import Data.Nat.Properties as NProp
import Data.Integer.Properties as ZProp

instance

*-ℕ : Semigroup _ _
*-ℕ = NProp.*-semigroup

*-â„€ : Semigroup _ _
*-â„€ = record { isSemigroup = ZProp.*-isSemigroup }

open import Data.Integer
open import Relation.Binary.PropositionalEquality

open OverloadedSemigroup {{...}}

abs-homomorphism : (m n : â„€) → ∣ m ∙ n ∣ ≡ ∣ m ∣ ∙ ∣ n ∣
abs-homomorphism m n = {!!}
===================================================================

Cheers,
--
gallais
Post by Sergei Meshveliani
Post by Martín Hötzel Escardó
Hi Sergei, I have a situation very similar to yours.
An ordinal is a type equipped with a relation _≺_ and a justification
that it is a well-order. Moreover, this order has an automatically
derived partial order _≌_.
If α is an ordinal, then I write ⟹ α ⟩ for the underlying type of α and
x ≺⟚ α ⟩ y and x ≌⟚ α ⟩ y for its underlying orders (given and derived).
The notation ⟹_⟩ for the underlying type is defined directly, just as a
projection.
The notations for the given and derived orders are given by "syntax"
declarations,
syntax underlying-order α x y = x ≺⟚ α ⟩ y
syntax underlying-porder α x y = x ≌⟚ α ⟩ y
where the underlying things are again projections.
I found that this worked quite well (although it would have been much
better if Agda could infer the "subscript" α for the orders, given that
x and y are known to live in the type ⟹ α ⟩).
Here are some examples from
http://www.cs.bham.ac.uk/~mhe/agda-new/OrdinalOfOrdinals.html
is-order-preserving
is-monotone
is-order-reflecting
is-order-embedding
is-order-equiv
is-initial-segment
is-simulation
: (α : Ordinal U) (β : Ordinal V) → (⟹ α ⟩ → ⟹ β ⟩) → U ⊔ V ̇
is-order-preserving α β f = (x y : ⟹ α ⟩) → x ≺⟚ α ⟩ y → f x ≺⟚ β ⟩ f y
is-monotone α β f = (x y : ⟹ α ⟩) → x ≌⟚ α ⟩ y → f x ≌⟚ β ⟩ f y
is-order-reflecting α β f = (x y : ⟹ α ⟩) → f x ≺⟚ β ⟩ f y → x ≺⟚ α ⟩ y
...
(Warning: I use U,V,W for type universes rather than "Set i" notation,
but this is another story. Additionally, U,V,W are "variables", a newly
introduced feature which is available in the development version only.)
I presume you could define a type "Setoid U" of setoids in the universe
U with very much the same underlying-type and underlying-equivalence
notation.
In my first reply I have probably confused things about universes.
Now I try once more to understand the idea.
Let us look at the result of this technique. Your demonstration shows
is-order-preserving α β f =
(x y : ⟹ α ⟩) → x ≺⟚ α ⟩ y → f x ≺⟚ β ⟩ f y
But the denotation ≺⟚ α ⟩ and ≺⟚ β ⟩ is not any better than
≺α and ≺β which uses renaming.
Am I missing something?
The goal is overloading. That is this signature needs to be
(x y : ⟹ α ⟩) → x ≺ y → f x ≺ f y (I)
According to the type of f, the first occurrence of ≺ needs to be
recognized by the type checker as on α and the second occurrence of ≺
needs to be recognized as on β.
Agda tends to be considered as an extension of Haskell.
But Haskell allows such overloading (to a certain extent) through the
mechanism of classes and instances. For example, (<), (+), (*).
are declared in Haskell library as certain class members, and are
overloaded like in (I).
I recall difficulties with constant operations and with overlapping
instances, but classes work there, to a certain extent.
Probably, the only remaining hope in Agda is for instance arguments,
something about the ``open ... {{...}}'' denotation.
I try it for Setoid._≈_, Semigroup._∙_, and it does not work.
Guillaume writes that to do this with respect to Standard library
operations, one needs to reorganize Standard library, a bit: to make
Carrier to be an argument to Setoid, and so on.
This means rewriting things in a certain programming style.
Regards,
------
Sergei
Post by Martín Hötzel Escardó
Post by Martín Hötzel Escardó
Post by Sergei Meshveliani
Post by James Wood
Agda doesn't do overloading for anything other than constructors, but
there are still tricks you can use. One I use a lot is making a local
module definition just to make a quick namespace, and then use dot
notation to access the contents of that module. In your example, it
module A = Setoid A
module B = Setoid B
IsCongruent : (A.Carrier → B.Carrier) → Set _
IsCongruent f = {x y} → x A.≈ y → (f x) B.≈ (f y)
Perhaps not ideal, but I've found it okay.
Thank you.
Currently I also use such in my example: P'.∙ε, P'.x∙x⁻¹, P'.∙cong2.
But it is essentially worse than ∙ε, x∙x⁻¹, ∙cong2.
I also have a renaming of ≈', which looks better than A.≈,
Also ≈ can be renamed to ≈A, which looks better than A.≈.
And all them are worse than ≈.
--
SM
Post by James Wood
Post by Sergei Meshveliani
Can anybody, please, explain how to arrange operation overloading
(something like classes) ?
The first example is
----------------------------------------------------------------
open import Level using (_⊔_)
open import Relation.Binary using (Setoid)
module _ {α α= β β=} (A : Setoid α α=) (B : Setoid β β=)
where
open Setoid -- {{...}}
C = Setoid.Carrier A
C' = Setoid.Carrier B
IsCongruent : (C → C') → Set _
IsCongruent f =
{x y : C} → _≈_ A x y → _≈_ B (f x) (f y) -- (I)
-- {x y : C} → x ≈ y → (f x) ≈ (f y) -- (II)
----------------------------------------------------------------
The line (I) does work.
Then I try the line (II), with un-commenting {{...}}.
And it is not type-checked.
I hoped for that it would find that the first ≈ is on C, while the
second ≈ is on C'. But it does not.
-----------------------------------------------------------------------
module _ {α α= β β=} (G : Group α α=) (G' : Group β β=)
where
...
(mHomo : MonoidHomomorphism)
(let f = MonoidHomomorphism.carryMap mHomo) (x : C) →
f (x ⁻¹) ≈' (f x) ⁻¹'
homomorphismPreservesInversion
(monoidHomo ((f , f-cong) , f∙homo) f-preserves-ε) x =
begin≈'
f x' ≈'[ ≈'sym (∙ε' fx') ]
fx' ∙' ε' ≈'[ ∙'cong2 (≈'sym (x∙'x⁻¹ fx)) ]
fx' ∙' (fx ∙' fx ⁻¹') ≈'[ ≈'sym (≈'assoc fx' fx (fx ⁻¹')) ]
(fx' ∙' fx) ∙' fx ⁻¹' ≈'[ ∙'cong1 (≈'sym (f∙homo x' x)) ]
f (x' ∙ x) ∙' fx ⁻¹' ≈'[ ∙'cong1 (f-cong (x⁻¹∙x x)) ]
f ε ∙' fx ⁻¹' ≈'[ ∙'cong1 f-preserves-ε ]
ε' ∙' fx ⁻¹' ≈'[ ε'∙ (fx ⁻¹') ]
(f x) ⁻¹'
end≈'
where
x' = x ⁻¹; fx = f x; fx' = f x'
----------------------------------------------------------------------
Here the carriers of G and G' are C and C',
≈ is on C, ≈' is on C' (by renaming),
_∙_ on C, _∙'_ on C',
ε is of G, ε' of G',
_⁻¹ is of G, _⁻¹' of G',
and so on.
It is desirable to make the code more readable by canceling some of the
above renaming. For example, to replace ε' with ε and _∙'_ with _∙_.
Is it possible to do this by using something like
open Group {{...}}
?
Thanks,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
--
http://www.cs.bham.ac.uk/~mhe
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Sergei Meshveliani
2018-11-12 18:05:38 UTC
Permalink
Post by Guillaume Brunerie
Hi Sergei,
Note that you don't the stdlib to change to be able to use Guillaume's
approach: you can add a layer on top of the stdlib giving a definition
of Semigroup exposing the Carrier and add a generic instance converting
===================================================================
open import Level
open import Algebra
open import Algebra.Structures
open import Algebra.FunctionProperties.Core
open import Relation.Binary
record OverloadedSemigroup {c} (Carrier : Set c) ℓ : Set (c ⊔ suc ℓ) where
infixl 7 _∙_
infix 4 _≈_
field
_≈_ : Rel Carrier ℓ
_∙_ : Op₂ Carrier
isSemigroup : IsSemigroup _≈_ _∙_
instance
OS : ∀ {c ℓ} {{S : Semigroup c ℓ}} →
OverloadedSemigroup (Semigroup.Carrier S) ℓ
OS {{S}} = record { Semigroup S }
import Data.Nat.Properties as NProp
import Data.Integer.Properties as ZProp
instance
*-ℕ : Semigroup _ _
*-ℕ = NProp.*-semigroup
*-ℤ : Semigroup _ _
*-ℤ = record { isSemigroup = ZProp.*-isSemigroup }
open import Data.Integer
open import Relation.Binary.PropositionalEquality
open OverloadedSemigroup {{...}}
abs-homomorphism : (m n : ℤ) → ∣ m ∙ n ∣ ≡ ∣ m ∣ ∙ ∣ n ∣
abs-homomorphism m n = {!!}
===================================================================
I thank both Guillaume-s for explanation.

Suppose that one develops a library for operating with fractions and
polynomials in general case. These functions will deal with various
different instances of the structures of Setoid, Semigroup, Monoid,
Group, ..., Semiring, CommutativeRing -- with different instances of
their declared operations and relations (_≈_, _∙_, _+_; _*_ and such).
Suppose that one needs to use in this library the same name for
different used instances for each of this operations.

I doubt of that this can be be totally supported.
Also some program fragments are read easier if there are used different
names.

Still let us put that we need to use such an overloading wide enough.
With your suggested approach, one needs to declare the `Overloaded'
version for each of the structures
Setoid, Semigroup, ..., Semiring, CommutativeRing.
Then, the library and user programs will be polluted with the prefix
`Overloaded'. I doubt of whether it worth to do this even if it is
abbreviated to a single letter `O'. A mathematician knows the word
Group, and one will be forced to find out what is OGroup.
I consider re-declaring structures like this:

record Setoid {c} ℓ (Carrier : Set c) : Set (suc (c ⊔ ℓ)) where
infix 4 _≈_
field
_≈_ : Rel Carrier ℓ
isEquivalence : IsEquivalence _≈_

-- after the suggestion by Guillaume Brunerie.
And if the user needs a Standard structure, one renames it to
Setoid-std, Semigroup-std, and so on.

Overloading for the above Setoid operations works like this:

open Setoid {{...}}

module _ {α α= β β=} (C : Set α) (C' : Set β)
{{S : Setoid α= C}} {{S' : Setoid β= C'}}
where
IsCongruent : (C → C') → Set _
IsCongruent f =
{x y : C} → x ≈ y → (f x) ≈ (f y)
-- --

(1) Can this approach be extended to further generic structures?

Also I do not understand the meaning of the `instance' language
construct.
I know its meaning in Haskell: an instance of a class.
I expect, that theoretically, this corresponds to a pair: a theory and
its model.
Now, Standard library for Agda declares, for example, Setoid
(which somewhat corresponds to some class) and also gives an
implementation for the Setoid instance for Nat (natural numbers)
-- without setting the word `instance'.
Also it gives an implementation to build the Setoid `pointwise' instance
for List A, from a Setoid instance over the type A -- without setting
the word `instance'.

(2) In the above intended `overloading' library where it will need to
appear the `instance' key word?

I thank people in advance for possible explanation.

------
Sergei
Guillaume Allais
2018-11-14 13:08:23 UTC
Permalink
You don't need to add the prefix `Overloaded` anywhere: you can merely
import `Algebra` (without opening it) and give your new structures the
same names as the ones in the standard library. You can then refer to the
ones in `Algebra` by using qualified names e.g. `Algebra.Monoid`.

`instance` is a bit like instance in Haskell: everything declared in the
block is made available for instance resolution. The difference in Agda
is of course that you can also declare record values *outside* of instance
blocks. They are then *not* used by the automatic instance resolution.
But the user can have access to them like any other value.

By default the standard library does not declare anything as an `instance`.
If you want resolution to use some of the structures made available in the
stdlib, you will need to put all of these into an instance block like I did
in my example for Nat and Integer.

Cheers,
--
gallais
Post by Sergei Meshveliani
Post by Guillaume Brunerie
Hi Sergei,
Note that you don't the stdlib to change to be able to use Guillaume's
approach: you can add a layer on top of the stdlib giving a definition
of Semigroup exposing the Carrier and add a generic instance converting
===================================================================
open import Level
open import Algebra
open import Algebra.Structures
open import Algebra.FunctionProperties.Core
open import Relation.Binary
record OverloadedSemigroup {c} (Carrier : Set c) ℓ : Set (c ⊔ suc ℓ) where
infixl 7 _∙_
infix 4 _≈_
field
_≈_ : Rel Carrier ℓ
_∙_ : Op₂ Carrier
isSemigroup : IsSemigroup _≈_ _∙_
instance
OS : ∀ {c ℓ} {{S : Semigroup c ℓ}} →
OverloadedSemigroup (Semigroup.Carrier S) ℓ
OS {{S}} = record { Semigroup S }
import Data.Nat.Properties as NProp
import Data.Integer.Properties as ZProp
instance
*-ℕ : Semigroup _ _
*-ℕ = NProp.*-semigroup
*-â„€ : Semigroup _ _
*-â„€ = record { isSemigroup = ZProp.*-isSemigroup }
open import Data.Integer
open import Relation.Binary.PropositionalEquality
open OverloadedSemigroup {{...}}
abs-homomorphism : (m n : â„€) → ∣ m ∙ n ∣ ≡ ∣ m ∣ ∙ ∣ n ∣
abs-homomorphism m n = {!!}
===================================================================
I thank both Guillaume-s for explanation.
Suppose that one develops a library for operating with fractions and
polynomials in general case. These functions will deal with various
different instances of the structures of Setoid, Semigroup, Monoid,
Group, ..., Semiring, CommutativeRing -- with different instances of
their declared operations and relations (_≈_, _∙_, _+_; _*_ and such).
Suppose that one needs to use in this library the same name for
different used instances for each of this operations.
I doubt of that this can be be totally supported.
Also some program fragments are read easier if there are used different
names.
Still let us put that we need to use such an overloading wide enough.
With your suggested approach, one needs to declare the `Overloaded'
version for each of the structures
Setoid, Semigroup, ..., Semiring, CommutativeRing.
Then, the library and user programs will be polluted with the prefix
`Overloaded'. I doubt of whether it worth to do this even if it is
abbreviated to a single letter `O'. A mathematician knows the word
Group, and one will be forced to find out what is OGroup.
record Setoid {c} ℓ (Carrier : Set c) : Set (suc (c ⊔ ℓ)) where
infix 4 _≈_
field
_≈_ : Rel Carrier ℓ
isEquivalence : IsEquivalence _≈_
-- after the suggestion by Guillaume Brunerie.
And if the user needs a Standard structure, one renames it to
Setoid-std, Semigroup-std, and so on.
open Setoid {{...}}
module _ {α α= β β=} (C : Set α) (C' : Set β)
{{S : Setoid α= C}} {{S' : Setoid β= C'}}
where
IsCongruent : (C → C') → Set _
IsCongruent f =
{x y : C} → x ≈ y → (f x) ≈ (f y)
-- --
(1) Can this approach be extended to further generic structures?
Also I do not understand the meaning of the `instance' language
construct.
I know its meaning in Haskell: an instance of a class.
I expect, that theoretically, this corresponds to a pair: a theory and
its model.
Now, Standard library for Agda declares, for example, Setoid
(which somewhat corresponds to some class) and also gives an
implementation for the Setoid instance for Nat (natural numbers)
-- without setting the word `instance'.
Also it gives an implementation to build the Setoid `pointwise' instance
for List A, from a Setoid instance over the type A -- without setting
the word `instance'.
(2) In the above intended `overloading' library where it will need to
appear the `instance' key word?
I thank people in advance for possible explanation.
------
Sergei
Sergei Meshveliani
2018-11-15 13:17:27 UTC
Permalink
Post by Guillaume Allais
[..]
`instance` is a bit like instance in Haskell: everything declared in the
block is made available for instance resolution. The difference in Agda
is of course that you can also declare record values *outside* of instance
blocks. They are then *not* used by the automatic instance resolution.
But the user can have access to them like any other value.
[..]
For example, I declare

record Setoid {c} ℓ (Carrier : Set c) : Set (suc (c ⊔ ℓ)) where
infix 4 _≈_
field
_≈_ : Rel Carrier ℓ
isEquivalence : IsEquivalence _≈_

(after the suggestion by Guillaume Brunerie).
Overloading for the above Setoid operations works like this:

open Setoid {{...}}

module _ {α α= β β=} (C : Set α) (C' : Set β)
{{S : Setoid α= C}} {{S' : Setoid β= C'}}
where
IsCongruent : (C → C') → Set _
IsCongruent f =
{x y : C} → x ≈ y → (f x) ≈ (f y)

The word `instance' is not applied.
On the other hand, the two instances for _≈_ are actually resolved.

For this particular declaration for Setoid, what possibility is lost by
skipping instance declarations?

Thanks,

------
Sergei
Guillaume Allais
2018-11-16 08:31:58 UTC
Permalink
You didn't use `instance` but you declared that the parameters S and S'
where instance arguments so they were used by the instance resolution.
This however only works for parameters. Ultimately you probably want
some concrete instances to be resolved. And that's where your `instance`
blocks matter.
Post by Sergei Meshveliani
Post by Guillaume Allais
[..]
`instance` is a bit like instance in Haskell: everything declared in the
block is made available for instance resolution. The difference in Agda
is of course that you can also declare record values *outside* of instance
blocks. They are then *not* used by the automatic instance resolution.
But the user can have access to them like any other value.
[..]
For example, I declare
record Setoid {c} ℓ (Carrier : Set c) : Set (suc (c ⊔ ℓ)) where
infix 4 _≈_
field
_≈_ : Rel Carrier ℓ
isEquivalence : IsEquivalence _≈_
(after the suggestion by Guillaume Brunerie).
open Setoid {{...}}
module _ {α α= β β=} (C : Set α) (C' : Set β)
{{S : Setoid α= C}} {{S' : Setoid β= C'}}
where
IsCongruent : (C → C') → Set _
IsCongruent f =
{x y : C} → x ≈ y → (f x) ≈ (f y)
The word `instance' is not applied.
On the other hand, the two instances for _≈_ are actually resolved.
For this particular declaration for Setoid, what possibility is lost by
skipping instance declarations?
Thanks,
------
Sergei
Sergei Meshveliani
2018-11-16 18:21:17 UTC
Permalink
Post by Guillaume Allais
You didn't use `instance` but you declared that the parameters S and S'
where instance arguments so they were used by the instance resolution.
This however only works for parameters. Ultimately you probably want
some concrete instances to be resolved. And that's where your `instance`
blocks matter.
I am trying to understand the thing by considering examples.
In the below example, I do not import Semigroup of Standard, instead
declare OSemigroup (after the sample given by Guillaume Brunerie).
(in a real program, I am going to redefine Semigroup as using Carrier as
argument, and Standard semigroup to be possible to imported with
renaming).

Then, define the instances of OSemigroup for (ℕ, _*_) and for A × B for
the pointwise operation.
Then, open OSemigroup {{...}}, and
use _∙_ to multiply both natural numbers and pairs of natural numbers,
use _≈_ both in 2 ∙ 3 ≈ 6 and in pair ≈ (4 , 6).

If I move oSemigroup-× out of the `instance' scope, then everything
is type-checked, except the last operations with `pair'.

This whole instance usage looks similar to Haskell's.

Is this a regular instance usage for Agda ?

Thanks,

------
Sergei


-----------------------------------------------------------------
open import Level
open import Algebra.FunctionProperties using (Op₂)
open import Algebra.Structures using (IsSemigroup)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

record OSemigroup {c} (Carrier : Set c) ℓ : Set (c ⊔ suc ℓ) where
infixl 7 _∙_
infix 4 _≈_
field
_≈_ : Rel Carrier ℓ
_∙_ : Op₂ Carrier
isSemigroup : IsSemigroup _≈_ _∙_


open import Data.Nat using (ℕ; _*_)
import Data.Nat.Properties as NProp
open import Data.Product using (_×_; _,_)
import Data.Product.Relation.Pointwise.NonDependent as PointwisePair

instance
*oSemigroup-ℕ : OSemigroup ℕ _
*oSemigroup-ℕ = record{ _≈_ = _≡_
; _∙_ = _*_
; isSemigroup = NProp.*-isSemigroup
}
oSemigroup-× : {c ℓ c' ℓ' : Level} {A : Set c} {B : Set c'} →
OSemigroup A ℓ → OSemigroup B ℓ' → OSemigroup (A × B) _

oSemigroup-× {c} {ℓ} {c'} {ℓ'} {A} {B} H H' =

record{ _≈_ = _≈_
; _∙_ = _∙_
; isSemigroup = A×B-isSemigroup
}
where
open OSemigroup H using () renaming (_≈_ to _≈₁_; _∙_ to _∙₁_)
open OSemigroup H' using () renaming (_≈_ to _≈₂_; _∙_ to _∙₂_)

_≈_ = PointwisePair.Pointwise _≈₁_ _≈₂_

_∙_ : Op₂ (A × B)
(x , y) ∙ (x' , y') = (x ∙₁ x' , y ∙₂ y')

postulate A×B-isSemigroup : IsSemigroup _≈_ _∙_

open OSemigroup {{...}}

eq1 : 2 ∙ 3 ≈ 6
eq1 = refl

pair : ℕ × ℕ
pair = (2 , 3) ∙ (2 , 2)

eq2 : pair ≈ (4 , 6)
eq2 = (refl , refl)
--------------------------------------------------------------------
Post by Guillaume Allais
Post by Sergei Meshveliani
Post by Guillaume Allais
[..]
`instance` is a bit like instance in Haskell: everything declared in the
block is made available for instance resolution. The difference in Agda
is of course that you can also declare record values *outside* of instance
blocks. They are then *not* used by the automatic instance resolution.
But the user can have access to them like any other value.
[..]
For example, I declare
record Setoid {c} ℓ (Carrier : Set c) : Set (suc (c ⊔ ℓ)) where
infix 4 _≈_
field
_≈_ : Rel Carrier ℓ
isEquivalence : IsEquivalence _≈_
(after the suggestion by Guillaume Brunerie).
open Setoid {{...}}
module _ {α α= β β=} (C : Set α) (C' : Set β)
{{S : Setoid α= C}} {{S' : Setoid β= C'}}
where
IsCongruent : (C → C') → Set _
IsCongruent f =
{x y : C} → x ≈ y → (f x) ≈ (f y)
The word `instance' is not applied.
On the other hand, the two instances for _≈_ are actually resolved.
For this particular declaration for Setoid, what possibility is lost by
skipping instance declarations?
Guillermo Calderon
2018-11-16 20:46:38 UTC
Permalink
Post by Sergei Meshveliani
Post by Guillaume Allais
You didn't use `instance` but you declared that the parameters S and S'
where instance arguments so they were used by the instance resolution.
This however only works for parameters. Ultimately you probably want
some concrete instances to be resolved. And that's where your `instance`
blocks matter.
I am trying to understand the thing by considering examples.
In the below example, I do not import Semigroup of Standard, instead
declare OSemigroup (after the sample given by Guillaume Brunerie).
(in a real program, I am going to redefine Semigroup as using Carrier as
argument, and Standard semigroup to be possible to imported with
renaming).
Actually, it is not necessary to declare the carrier as a parameter of
the record to work with instances, overloading and this stuff.

See my post bellow in this thread and the next mesage of Guillaume.
Post by Sergei Meshveliani
Then, define the instances of OSemigroup for (ℕ, _*_) and for A × B for
the pointwise operation.
Then, open OSemigroup {{...}}, and
use _∙_ to multiply both natural numbers and pairs of natural numbers,
use _≈_ both in 2 ∙ 3 ≈ 6 and in pair ≈ (4 , 6).
If I move oSemigroup-× out of the `instance' scope, then everything
is type-checked, except the last operations with `pair'.
This whole instance usage looks similar to Haskell's.
Is this a regular instance usage for Agda ?
Thanks,
------
Sergei
-----------------------------------------------------------------
open import Level
open import Algebra.FunctionProperties using (Op₂)
open import Algebra.Structures using (IsSemigroup)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
record OSemigroup {c} (Carrier : Set c) ℓ : Set (c ⊔ suc ℓ) where
infixl 7 _∙_
infix 4 _≈_
field
_≈_ : Rel Carrier ℓ
_∙_ : Op₂ Carrier
isSemigroup : IsSemigroup _≈_ _∙_
open import Data.Nat using (ℕ; _*_)
import Data.Nat.Properties as NProp
open import Data.Product using (_×_; _,_)
import Data.Product.Relation.Pointwise.NonDependent as PointwisePair
instance
*oSemigroup-ℕ : OSemigroup ℕ _
*oSemigroup-ℕ = record{ _≈_ = _≡_
; _∙_ = _*_
; isSemigroup = NProp.*-isSemigroup
}
oSemigroup-× : {c ℓ c' ℓ' : Level} {A : Set c} {B : Set c'} →
OSemigroup A ℓ → OSemigroup B ℓ' → OSemigroup (A × B) _
oSemigroup-× {c} {ℓ} {c'} {ℓ'} {A} {B} H H' =
record{ _≈_ = _≈_
; _∙_ = _∙_
; isSemigroup = A×B-isSemigroup
}
where
open OSemigroup H using () renaming (_≈_ to _≈₁_; _∙_ to _∙₁_)
open OSemigroup H' using () renaming (_≈_ to _≈₂_; _∙_ to _∙₂_)
_≈_ = PointwisePair.Pointwise _≈₁_ _≈₂_
_∙_ : Op₂ (A × B)
(x , y) ∙ (x' , y') = (x ∙₁ x' , y ∙₂ y')
postulate A×B-isSemigroup : IsSemigroup _≈_ _∙_
open OSemigroup {{...}}
eq1 : 2 ∙ 3 ≈ 6
eq1 = refl
pair : ℕ × ℕ
pair = (2 , 3) ∙ (2 , 2)
eq2 : pair ≈ (4 , 6)
eq2 = (refl , refl)
--------------------------------------------------------------------
Post by Guillaume Allais
Post by Sergei Meshveliani
Post by Guillaume Allais
[..]
`instance` is a bit like instance in Haskell: everything declared in the
block is made available for instance resolution. The difference in Agda
is of course that you can also declare record values *outside* of instance
blocks. They are then *not* used by the automatic instance resolution.
But the user can have access to them like any other value.
[..]
For example, I declare
record Setoid {c} ℓ (Carrier : Set c) : Set (suc (c ⊔ ℓ)) where
infix 4 _≈_
field
_≈_ : Rel Carrier ℓ
isEquivalence : IsEquivalence _≈_
(after the suggestion by Guillaume Brunerie).
open Setoid {{...}}
module _ {α α= β β=} (C : Set α) (C' : Set β)
{{S : Setoid α= C}} {{S' : Setoid β= C'}}
where
IsCongruent : (C → C') → Set _
IsCongruent f =
{x y : C} → x ≈ y → (f x) ≈ (f y)
The word `instance' is not applied.
On the other hand, the two instances for _≈_ are actually resolved.
For this particular declaration for Setoid, what possibility is lost by
skipping instance declarations?
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Sergei Meshveliani
2018-11-09 20:44:02 UTC
Permalink
Post by Martín Hötzel Escardó
Hi Sergei, I have a situation very similar to yours.
An ordinal is a type equipped with a relation _≺_ and a justification
that it is a well-order. Moreover, this order has an automatically
derived partial order _≼_.
If α is an ordinal, then I write ⟨ α ⟩ for the underlying type of α and
x ≺⟨ α ⟩ y and x ≼⟨ α ⟩ y for its underlying orders (given and derived).
The notation ⟨_⟩ for the underlying type is defined directly, just as a
projection.
The notations for the given and derived orders are given by "syntax"
declarations,
syntax underlying-order α x y = x ≺⟨ α ⟩ y
syntax underlying-porder α x y = x ≼⟨ α ⟩ y
where the underlying things are again projections.
I found that this worked quite well (although it would have been much
better if Agda could infer the "subscript" α for the orders, given that
x and y are known to live in the type ⟨ α ⟩).
Here are some examples from
http://www.cs.bham.ac.uk/~mhe/agda-new/OrdinalOfOrdinals.html
is-order-preserving
is-monotone
is-order-reflecting
is-order-embedding
is-order-equiv
is-initial-segment
is-simulation
: (α : Ordinal U) (β : Ordinal V) → (⟨ α ⟩ → ⟨ β ⟩) → U ⊔ V ̇
is-order-preserving α β f = (x y : ⟨ α ⟩) → x ≺⟨ α ⟩ y → f x ≺⟨ β ⟩ f y
is-monotone α β f = (x y : ⟨ α ⟩) → x ≼⟨ α ⟩ y → f x ≼⟨ β ⟩ f y
is-order-reflecting α β f = (x y : ⟨ α ⟩) → f x ≺⟨ β ⟩ f y → x ≺⟨ α ⟩ y
...
(Warning: I use U,V,W for type universes rather than "Set i" notation,
but this is another story. Additionally, U,V,W are "variables", a newly
introduced feature which is available in the development version only.)
I presume you could define a type "Setoid U" of setoids in the universe
U with very much the same underlying-type and underlying-equivalence
notation.
Thank you.
1) I need to study using `syntax'.
(is this thing essential for the subject?)

2) What is "type universe" ?
Is it the Universe programming technique introduced in the book
by Norell & Chapman ?

"A universe is a set of types (or type formers) and a universe
construction consists of a type of codes and a decoding function mapping
codes to types in the universe.
...
"
I never tried this thing. Is it essential for the subject?

3) Really, will it also support overloading for the operations
_∙_, _⁻¹, _+_ in Group, Ring and such structures of Standard
library ?

Regards,

------
Sergei
Post by Martín Hötzel Escardó
[..]
Post by Sergei Meshveliani
Post by Sergei Meshveliani
Can anybody, please, explain how to arrange operation overloading
(something like classes) ?
The first example is
----------------------------------------------------------------
open import Level using (_⊔_)
open import Relation.Binary using (Setoid)
module _ {α α= β β=} (A : Setoid α α=) (B : Setoid β β=)
where
open Setoid -- {{...}}
C = Setoid.Carrier A
C' = Setoid.Carrier B
IsCongruent : (C → C') → Set _
IsCongruent f =
{x y : C} → _≈_ A x y → _≈_ B (f x) (f y) -- (I)
-- {x y : C} → x ≈ y → (f x) ≈ (f y) -- (II)
----------------------------------------------------------------
The line (I) does work.
Then I try the line (II), with un-commenting {{...}}.
And it is not type-checked.
I hoped for that it would find that the first ≈ is on C, while the
second ≈ is on C'. But it does not.
-----------------------------------------------------------------------
module _ {α α= β β=} (G : Group α α=) (G' : Group β β=)
where
...
(mHomo : MonoidHomomorphism)
(let f = MonoidHomomorphism.carryMap mHomo) (x : C) →
f (x ⁻¹) ≈' (f x) ⁻¹'
homomorphismPreservesInversion
(monoidHomo ((f , f-cong) , f∙homo) f-preserves-ε) x =
begin≈'
f x' ≈'[ ≈'sym (∙ε' fx') ]
fx' ∙' ε' ≈'[ ∙'cong2 (≈'sym (x∙'x⁻¹ fx)) ]
fx' ∙' (fx ∙' fx ⁻¹') ≈'[ ≈'sym (≈'assoc fx' fx (fx ⁻¹')) ]
(fx' ∙' fx) ∙' fx ⁻¹' ≈'[ ∙'cong1 (≈'sym (f∙homo x' x)) ]
f (x' ∙ x) ∙' fx ⁻¹' ≈'[ ∙'cong1 (f-cong (x⁻¹∙x x)) ]
f ε ∙' fx ⁻¹' ≈'[ ∙'cong1 f-preserves-ε ]
ε' ∙' fx ⁻¹' ≈'[ ε'∙ (fx ⁻¹') ]
(f x) ⁻¹'
end≈'
where
x' = x ⁻¹; fx = f x; fx' = f x'
----------------------------------------------------------------------
Here the carriers of G and G' are C and C',
≈ is on C, ≈' is on C' (by renaming),
_∙_ on C, _∙'_ on C',
ε is of G, ε' of G',
_⁻¹ is of G, _⁻¹' of G',
and so on.
It is desirable to make the code more readable by canceling some of the
above renaming. For example, to replace ε' with ε and _∙'_ with _∙_.
Is it possible to do this by using something like
open Group {{...}}
?
Thanks,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Guillaume Brunerie
2018-11-09 20:50:56 UTC
Permalink
Post by Sergei Meshveliani
3) Really, will it also support overloading for the operations
_∙_, _⁻¹, _+_ in Group, Ring and such structures of Standard
library ?
Ideally yes, although I don’t know if anyone actually tried.
There seems to be some of it in agda-prelude (for instance Monoid and
SemiRing), but it seems less developed than the standard library (I
couldn’t find Group or Ring, for instance).
Post by Sergei Meshveliani
[..]
Post by Sergei Meshveliani
Post by Sergei Meshveliani
Can anybody, please, explain how to arrange operation overloading
(something like classes) ?
The first example is
----------------------------------------------------------------
open import Level using (_⊔_)
open import Relation.Binary using (Setoid)
module _ {α α= β β=} (A : Setoid α α=) (B : Setoid β β=)
where
open Setoid -- {{...}}
C = Setoid.Carrier A
C' = Setoid.Carrier B
IsCongruent : (C → C') → Set _
IsCongruent f =
{x y : C} → _≈_ A x y → _≈_ B (f x) (f y) -- (I)
-- {x y : C} → x ≈ y → (f x) ≈ (f y) -- (II)
----------------------------------------------------------------
The line (I) does work.
Then I try the line (II), with un-commenting {{...}}.
And it is not type-checked.
I hoped for that it would find that the first ≈ is on C, while the
second ≈ is on C'. But it does not.
-----------------------------------------------------------------------
module _ {α α= β β=} (G : Group α α=) (G' : Group β β=)
where
...
(mHomo : MonoidHomomorphism)
(let f = MonoidHomomorphism.carryMap mHomo) (x : C) →
f (x ⁻¹) ≈' (f x) ⁻¹'
homomorphismPreservesInversion
(monoidHomo ((f , f-cong) , f∙homo) f-preserves-ε) x =
begin≈'
f x' ≈'[ ≈'sym (∙ε' fx') ]
fx' ∙' ε' ≈'[ ∙'cong2 (≈'sym (x∙'x⁻¹ fx)) ]
fx' ∙' (fx ∙' fx ⁻¹') ≈'[ ≈'sym (≈'assoc fx' fx (fx ⁻¹')) ]
(fx' ∙' fx) ∙' fx ⁻¹' ≈'[ ∙'cong1 (≈'sym (f∙homo x' x)) ]
f (x' ∙ x) ∙' fx ⁻¹' ≈'[ ∙'cong1 (f-cong (x⁻¹∙x x)) ]
f ε ∙' fx ⁻¹' ≈'[ ∙'cong1 f-preserves-ε ]
ε' ∙' fx ⁻¹' ≈'[ ε'∙ (fx ⁻¹') ]
(f x) ⁻¹'
end≈'
where
x' = x ⁻¹; fx = f x; fx' = f x'
----------------------------------------------------------------------
Here the carriers of G and G' are C and C',
≈ is on C, ≈' is on C' (by renaming),
_∙_ on C, _∙'_ on C',
ε is of G, ε' of G',
_⁻¹ is of G, _⁻¹' of G',
and so on.
It is desirable to make the code more readable by canceling some of the
above renaming. For example, to replace ε' with ε and _∙'_ with _∙_.
Is it possible to do this by using something like
open Group {{...}}
?
Thanks,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Guillaume Brunerie
2018-11-09 17:46:10 UTC
Permalink
Hi Sergei,

Unless I missed something, it does not seem possible to do what you
want because of the way setoids are set up in the standard library. In
order for instance arguments to work, you need an IsSetoid type taking
the carrier type as an argument (rather than a Setoid module having
the carrier type as a field). Here is how it would work:


open import Level using (suc; _⊔_)
open import Relation.Binary using (Rel; IsEquivalence)

record IsSetoid {c} ℓ (Carrier : Set c) : Set (suc (c ⊔ ℓ)) where
infix 4 _≈_
field
_≈_ : Rel Carrier ℓ
isEquivalence : IsEquivalence _≈_

open IsSetoid {{...}}

module _ {α α= β β=} (A : Set α) {{A-setoid : IsSetoid α= A}} (B : Set
β) {{B-setoid : IsSetoid β= B}}
where

IsCongruent : (A → B) → Set _
IsCongruent f = {x y : A} → x ≈ y → (f x) ≈ (f y)


Best,
Guillaume
Post by Sergei Meshveliani
Can anybody, please, explain how to arrange operation overloading
(something like classes) ?
The first example is
----------------------------------------------------------------
open import Level using (_⊔_)
open import Relation.Binary using (Setoid)
module _ {α α= β β=} (A : Setoid α α=) (B : Setoid β β=)
where
open Setoid -- {{...}}
C = Setoid.Carrier A
C' = Setoid.Carrier B
IsCongruent : (C → C') → Set _
IsCongruent f =
{x y : C} → _≈_ A x y → _≈_ B (f x) (f y) -- (I)
-- {x y : C} → x ≈ y → (f x) ≈ (f y) -- (II)
----------------------------------------------------------------
The line (I) does work.
Then I try the line (II), with un-commenting {{...}}.
And it is not type-checked.
I hoped for that it would find that the first ≈ is on C, while the
second ≈ is on C'. But it does not.
-----------------------------------------------------------------------
module _ {α α= β β=} (G : Group α α=) (G' : Group β β=)
where
...
(mHomo : MonoidHomomorphism)
(let f = MonoidHomomorphism.carryMap mHomo) (x : C) →
f (x ⁻¹) ≈' (f x) ⁻¹'
homomorphismPreservesInversion
(monoidHomo ((f , f-cong) , f∙homo) f-preserves-ε) x =
begin≈'
f x' ≈'[ ≈'sym (∙ε' fx') ]
fx' ∙' ε' ≈'[ ∙'cong2 (≈'sym (x∙'x⁻¹ fx)) ]
fx' ∙' (fx ∙' fx ⁻¹') ≈'[ ≈'sym (≈'assoc fx' fx (fx ⁻¹')) ]
(fx' ∙' fx) ∙' fx ⁻¹' ≈'[ ∙'cong1 (≈'sym (f∙homo x' x)) ]
f (x' ∙ x) ∙' fx ⁻¹' ≈'[ ∙'cong1 (f-cong (x⁻¹∙x x)) ]
f ε ∙' fx ⁻¹' ≈'[ ∙'cong1 f-preserves-ε ]
ε' ∙' fx ⁻¹' ≈'[ ε'∙ (fx ⁻¹') ]
(f x) ⁻¹'
end≈'
where
x' = x ⁻¹; fx = f x; fx' = f x'
----------------------------------------------------------------------
Here the carriers of G and G' are C and C',
≈ is on C, ≈' is on C' (by renaming),
_∙_ on C, _∙'_ on C',
ε is of G, ε' of G',
_⁻¹ is of G, _⁻¹' of G',
and so on.
It is desirable to make the code more readable by canceling some of the
above renaming. For example, to replace ε' with ε and _∙'_ with _∙_.
Is it possible to do this by using something like
open Group {{...}}
?
Thanks,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Sergei Meshveliani
2018-11-09 19:41:41 UTC
Permalink
Post by Guillaume Brunerie
Hi Sergei,
Unless I missed something, it does not seem possible to do what you
want because of the way setoids are set up in the standard library. In
order for instance arguments to work, you need an IsSetoid type taking
the carrier type as an argument (rather than a Setoid module having
open import Level using (suc; _⊔_)
open import Relation.Binary using (Rel; IsEquivalence)
record IsSetoid {c} ℓ (Carrier : Set c) : Set (suc (c ⊔ ℓ)) where
infix 4 _≈_
field
_≈_ : Rel Carrier ℓ
isEquivalence : IsEquivalence _≈_
open IsSetoid {{...}}
module _ {α α= β β=} (A : Set α) {{A-setoid : IsSetoid α= A}} (B : Set
β) {{B-setoid : IsSetoid β= B}}
where
IsCongruent : (A → B) → Set _
IsCongruent f = {x y : A} → x ≈ y → (f x) ≈ (f y)
Thank you.
Imagine the version lib-II of Standard library which defines IsSetoid
this way.
How many changes will this cause in the definitions in the classical
algebra structures: Setoid, Semigroup, Monoid ... CommutativeRing
?
Will _∙_ of Semigroup, _⁻¹ of Group, _+_ of Ring, and such,
become overloadable?

Anybody tried such a library?

Thanks,

------
Sergei
Post by Guillaume Brunerie
Post by Sergei Meshveliani
Can anybody, please, explain how to arrange operation overloading
(something like classes) ?
The first example is
----------------------------------------------------------------
open import Level using (_⊔_)
open import Relation.Binary using (Setoid)
module _ {α α= β β=} (A : Setoid α α=) (B : Setoid β β=)
where
open Setoid -- {{...}}
C = Setoid.Carrier A
C' = Setoid.Carrier B
IsCongruent : (C → C') → Set _
IsCongruent f =
{x y : C} → _≈_ A x y → _≈_ B (f x) (f y) -- (I)
-- {x y : C} → x ≈ y → (f x) ≈ (f y) -- (II)
----------------------------------------------------------------
The line (I) does work.
Then I try the line (II), with un-commenting {{...}}.
And it is not type-checked.
I hoped for that it would find that the first ≈ is on C, while the
second ≈ is on C'. But it does not.
-----------------------------------------------------------------------
module _ {α α= β β=} (G : Group α α=) (G' : Group β β=)
where
...
(mHomo : MonoidHomomorphism)
(let f = MonoidHomomorphism.carryMap mHomo) (x : C) →
f (x ⁻¹) ≈' (f x) ⁻¹'
homomorphismPreservesInversion
(monoidHomo ((f , f-cong) , f∙homo) f-preserves-ε) x =
begin≈'
f x' ≈'[ ≈'sym (∙ε' fx') ]
fx' ∙' ε' ≈'[ ∙'cong2 (≈'sym (x∙'x⁻¹ fx)) ]
fx' ∙' (fx ∙' fx ⁻¹') ≈'[ ≈'sym (≈'assoc fx' fx (fx ⁻¹')) ]
(fx' ∙' fx) ∙' fx ⁻¹' ≈'[ ∙'cong1 (≈'sym (f∙homo x' x)) ]
f (x' ∙ x) ∙' fx ⁻¹' ≈'[ ∙'cong1 (f-cong (x⁻¹∙x x)) ]
f ε ∙' fx ⁻¹' ≈'[ ∙'cong1 f-preserves-ε ]
ε' ∙' fx ⁻¹' ≈'[ ε'∙ (fx ⁻¹') ]
(f x) ⁻¹'
end≈'
where
x' = x ⁻¹; fx = f x; fx' = f x'
----------------------------------------------------------------------
Here the carriers of G and G' are C and C',
≈ is on C, ≈' is on C' (by renaming),
_∙_ on C, _∙'_ on C',
ε is of G, ε' of G',
_⁻¹ is of G, _⁻¹' of G',
and so on.
It is desirable to make the code more readable by canceling some of the
above renaming. For example, to replace ε' with ε and _∙'_ with _∙_.
Is it possible to do this by using something like
open Group {{...}}
?
Thanks,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Guillermo Calderon
2018-11-14 15:10:03 UTC
Permalink
Hi,

This works:

```
...

open Setoid {{...}}

instance
A' : Setoid α α=
A' = A

B' : Setoid β β=
B' = B

C = Setoid.Carrier A
C' = Setoid.Carrier B

IsCongruent : (C → C') → Set _
IsCongruent f = {x y : C} → x ≈ y → (f x) ≈ (f y) -- (II)

```

Unfortunately, I have to introduce dummy identifiers A' and B' in order
to declare the instances. Perhaps, there exists a way to avoid it.

Regards,

Guillermo
Post by Sergei Meshveliani
Can anybody, please, explain how to arrange operation overloading
(something like classes) ?
The first example is
----------------------------------------------------------------
open import Level using (_⊔_)
open import Relation.Binary using (Setoid)
module _ {α α= β β=} (A : Setoid α α=) (B : Setoid β β=)
where
open Setoid -- {{...}}
C = Setoid.Carrier A
C' = Setoid.Carrier B
IsCongruent : (C → C') → Set _
IsCongruent f =
{x y : C} → _≈_ A x y → _≈_ B (f x) (f y) -- (I)
-- {x y : C} → x ≈ y → (f x) ≈ (f y) -- (II)
----------------------------------------------------------------
The line (I) does work.
Then I try the line (II), with un-commenting {{...}}.
And it is not type-checked.
I hoped for that it would find that the first ≈ is on C, while the
second ≈ is on C'. But it does not.
-----------------------------------------------------------------------
module _ {α α= β β=} (G : Group α α=) (G' : Group β β=)
where
...
(mHomo : MonoidHomomorphism)
(let f = MonoidHomomorphism.carryMap mHomo) (x : C) →
f (x ⁻¹) ≈' (f x) ⁻¹'
homomorphismPreservesInversion
(monoidHomo ((f , f-cong) , f∙homo) f-preserves-ε) x =
begin≈'
f x' ≈'[ ≈'sym (∙ε' fx') ]
fx' ∙' ε' ≈'[ ∙'cong2 (≈'sym (x∙'x⁻¹ fx)) ]
fx' ∙' (fx ∙' fx ⁻¹') ≈'[ ≈'sym (≈'assoc fx' fx (fx ⁻¹')) ]
(fx' ∙' fx) ∙' fx ⁻¹' ≈'[ ∙'cong1 (≈'sym (f∙homo x' x)) ]
f (x' ∙ x) ∙' fx ⁻¹' ≈'[ ∙'cong1 (f-cong (x⁻¹∙x x)) ]
f ε ∙' fx ⁻¹' ≈'[ ∙'cong1 f-preserves-ε ]
ε' ∙' fx ⁻¹' ≈'[ ε'∙ (fx ⁻¹') ]
(f x) ⁻¹'
end≈'
where
x' = x ⁻¹; fx = f x; fx' = f x'
----------------------------------------------------------------------
Here the carriers of G and G' are C and C',
≈ is on C, ≈' is on C' (by renaming),
_∙_ on C, _∙'_ on C',
ε is of G, ε' of G',
_⁻¹ is of G, _⁻¹' of G',
and so on.
It is desirable to make the code more readable by canceling some of the
above renaming. For example, to replace ε' with ε and _∙'_ with _∙_.
Is it possible to do this by using something like
open Group {{...}}
?
Thanks,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Guillaume Brunerie
2018-11-14 15:20:19 UTC
Permalink
Oh, nice! It’s much simpler than I thought.

You can use anonymous declarations to get rid of the dummy
identifiers, and you don’t have to write their types.
So the whole instance block can be shortened to

instance
_ = A
_ = B

Alternatively, if A and B are instance arguments of the module, then
there is not need for an instance block at all.

Best,
Guillaume
Post by Guillermo Calderon
Hi,
```
...
open Setoid {{...}}
instance
A' : Setoid α α=
A' = A
B' : Setoid β β=
B' = B
C = Setoid.Carrier A
C' = Setoid.Carrier B
IsCongruent : (C → C') → Set _
IsCongruent f = {x y : C} → x ≈ y → (f x) ≈ (f y) -- (II)
```
Unfortunately, I have to introduce dummy identifiers A' and B' in order
to declare the instances. Perhaps, there exists a way to avoid it.
Regards,
Guillermo
Post by Sergei Meshveliani
Can anybody, please, explain how to arrange operation overloading
(something like classes) ?
The first example is
----------------------------------------------------------------
open import Level using (_⊔_)
open import Relation.Binary using (Setoid)
module _ {α α= β β=} (A : Setoid α α=) (B : Setoid β β=)
where
open Setoid -- {{...}}
C = Setoid.Carrier A
C' = Setoid.Carrier B
IsCongruent : (C → C') → Set _
IsCongruent f =
{x y : C} → _≈_ A x y → _≈_ B (f x) (f y) -- (I)
-- {x y : C} → x ≈ y → (f x) ≈ (f y) -- (II)
----------------------------------------------------------------
The line (I) does work.
Then I try the line (II), with un-commenting {{...}}.
And it is not type-checked.
I hoped for that it would find that the first ≈ is on C, while the
second ≈ is on C'. But it does not.
-----------------------------------------------------------------------
module _ {α α= β β=} (G : Group α α=) (G' : Group β β=)
where
...
(mHomo : MonoidHomomorphism)
(let f = MonoidHomomorphism.carryMap mHomo) (x : C) →
f (x ⁻¹) ≈' (f x) ⁻¹'
homomorphismPreservesInversion
(monoidHomo ((f , f-cong) , f∙homo) f-preserves-ε) x =
begin≈'
f x' ≈'[ ≈'sym (∙ε' fx') ]
fx' ∙' ε' ≈'[ ∙'cong2 (≈'sym (x∙'x⁻¹ fx)) ]
fx' ∙' (fx ∙' fx ⁻¹') ≈'[ ≈'sym (≈'assoc fx' fx (fx ⁻¹')) ]
(fx' ∙' fx) ∙' fx ⁻¹' ≈'[ ∙'cong1 (≈'sym (f∙homo x' x)) ]
f (x' ∙ x) ∙' fx ⁻¹' ≈'[ ∙'cong1 (f-cong (x⁻¹∙x x)) ]
f ε ∙' fx ⁻¹' ≈'[ ∙'cong1 f-preserves-ε ]
ε' ∙' fx ⁻¹' ≈'[ ε'∙ (fx ⁻¹') ]
(f x) ⁻¹'
end≈'
where
x' = x ⁻¹; fx = f x; fx' = f x'
----------------------------------------------------------------------
Here the carriers of G and G' are C and C',
≈ is on C, ≈' is on C' (by renaming),
_∙_ on C, _∙'_ on C',
ε is of G, ε' of G',
_⁻¹ is of G, _⁻¹' of G',
and so on.
It is desirable to make the code more readable by canceling some of the
above renaming. For example, to replace ε' with ε and _∙'_ with _∙_.
Is it possible to do this by using something like
open Group {{...}}
?
Thanks,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Loading...