Add coercions

[UlfNorell]

From guillaum...@gmail.com on November 06, 2012 17:53:53

I’d like to have coercions in Agda. I don’t know much about coercions apart from what is implemented in Coq (see http://coq.inria.fr/refman/Reference-Manual023.html )

As far as I understand, there are basically three types of coercions:

• Sort coercions, you have a family of types [D params], a term [coerce] of type [forall params -> D params -> Set i], and you have declared [coerce] to be a coercion from [D] to [Sortclass](in Coq terminology) Now if you have [A : D params], you can write [x : A] and this is automatically translated to [x : coerce params A]
• Function coercions, you have a family of types [D params], a term [coerce] of type [forall params -> D params -> (A -> B)], and you have declared [coerce] to be a coercion from [D] to [Funclass](in Coq terminology) Now if you have [f : D params] and [x : A], you can write [f x] and this is automatically translated to [(coerce params f) x]
• Other coercions, you have two families of types [D params] and [E params'], a term [coerce] of type [forall params -> D params -> E params'], and you have declared [coerce] to be a coercion from [D] to [E] Now if you have [x : D params] and you need something of type [E params'], you can just write [x] and this is automatically translated to [coerce params x]

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

[UlfNorell]

From andreas....@gmail.com on November 06, 2012 11:51:26

Coercions is probably a good thing to have, but in the mean time you could maybe try type classes. For instance, function coercions can be implemented by an overloaded application operator. This is not like in Scala, where the actual application can be overloaded, but at least it looks still light-weight:

open import Common.Prelude renaming (Nat to ℕ)

-- Apply type class

record Apply (C : Set) (A : Set) (B : A → Set) : Set where field apply : C → (x : A) → B x

-- overloaded application

$ : ∀ {C A}{B : A → Set} → C → {{app : Apply C A B}} → (x : A) → B x $ f {{app}} = Apply.apply app f

-- my custom type of functions

record NatFun : Set where field theFun : ℕ → ℕ

-- application instance

natFunApply : Apply NatFun ℕ (λ n → ℕ) natFunApply = record { apply = NatFun.theFun }

myNatFun : NatFun myNatFun = record { theFun = suc }

test = myNatFun $ 5

Status: InfoNeeded
Labels: Type-Enhancement

[UlfNorell]

From guillaum...@gmail.com on November 14, 2012 07:15:03

Yes, I know that I can define such an overloaded application operator but I’d like to be able to overload the actual application.

Also, in something I’m doing I would like to have a type ℕ of natural numbers, a type ℕ₋₁ of integers ≥ -1 and a type ℕ₋₂ of integers ≥ -2, and to be able to write -2, -1, 0, 1, etc. for terms of any of these three types (when it makes sense) and to have maps adding 1 and removing 1 with the correct types. Doing it with explicit coercions seems a bit messy.

[UlfNorell]

From nils.anders.danielsson on November 14, 2012 07:57:17

Also, in something I’m doing I would like to have a type ℕ of natural numbers, a type ℕ₋₁ of integers ≥ -1 and a type ℕ₋₂ of integers ≥ -2, [...]

Homotopy type theory? This sounds like asking for trouble. Why not simply number from zero (except to conform to the notation of some other community)? One option is to do something like the following:

open Prelude public using () renaming (zero to [-1])

[0] = suc [-1] [1] = suc [0] [2] = suc [1] [3] = suc [2]

open Prelude public using () renaming (zero to ⟨-2⟩)

⟨-1⟩ = suc ⟨-2⟩ ⟨0⟩ = suc ⟨-1⟩ ⟨1⟩ = suc ⟨0⟩ ⟨2⟩ = suc ⟨1⟩

[UlfNorell]

From nils.anders.danielsson on November 14, 2012 07:59:44

Slightly better:

open Prelude public using () renaming (zero to [-1])

[_] : ℕ → ℕ [ n ] = suc n

open Prelude public using () renaming (zero to ⟨-2⟩)

⟨-1⟩ = suc ⟨-2⟩

⟨_⟩ : ℕ → ℕ ⟨ n ⟩ = suc (suc n)

[UlfNorell]

From guillaum...@gmail.com on November 14, 2012 10:27:18

Homotopy type theory?

Yes. The problem is that I want to say something like "Filling all maps from the n-dimensional sphere to A gives the (n-1)-truncation of A". And in usual homotopy theory, the spheres are numbered starting at -1 (the (-1)-sphere being empty) and the truncation levels are numbered starting at -2.

For now I’m saying that "Filling all maps from the n-dimensional sphere' to A gives the n-truncation' of A" where sphere' is sphere with a numbering off by one, and truncation' is the truncation with a numbering off by two. Similarly I would like to replace the notion of "being of h-level n" with "being (n-2)-truncated", in order to be closer to ordinary homotopy theory.

Thank for the workaround, I’ll try it to see if that’s enough and perhaps remove the (-1)-sphere in order to start the numbering of spheres at 0.

[UlfNorell]

From guillaum...@gmail.com on March 07, 2013 06:16:24

I solved my problem of numbering, but coercions would still be very useful. In particular, working in homotopy type theory with pointed types is very painful now because you have to distinguish all the time between the pointed type and the type itself, and even trying to use some lightweight notation becomes quickly very heavy.