Add coercions

[GoogleCodeExporter]

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 reported on code.google.com by guillaum...@gmail.com on 6 Nov 2012 at 4:53

[GoogleCodeExporter]

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

Original comment by andreas....@gmail.com on 6 Nov 2012 at 7:51

• Changed state: InfoNeeded
• Added labels: Type-Enhancement

[GoogleCodeExporter]

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.

Original comment by guillaum...@gmail.com on 14 Nov 2012 at 3:15

[GoogleCodeExporter]

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⟩

Original comment by nils.anders.danielsson on 14 Nov 2012 at 3:57

[GoogleCodeExporter]

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)

Original comment by nils.anders.danielsson on 14 Nov 2012 at 3:59

[GoogleCodeExporter]

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.

Original comment by guillaum...@gmail.com on 14 Nov 2012 at 6:27

[GoogleCodeExporter]

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.

Original comment by guillaum...@gmail.com on 7 Mar 2013 at 2:16

[UlfNorell]

I strongly suspect adding coercions would completely wreck constraint solving. Coq isn't as picky about unique solutions and can get away with more clever heuristics.

[jespercockx]

Funny, I was just discussing coercions with the Coq people here in Nantes as a possible way to implement cumulativity. It seems to me that we could get away with having some coercions if we would distinguish more carefully in the typechecker when we expect the type to match exactly and when any supertype will do (for example, by adopting a more bidirectional approach).

Do you have any hard evidence that this would destroy Agda's constraint solver irredeemably, or is it just a suspicion?

[UlfNorell]

No hard evidence, no. But let's do a little exploratory example:

postulate
  A B : Set

postulate
  coerce : A → B

id : (A : Set) → A → A
id x = x

foo : A → B
foo x = let X = _ in id X x

Now what's the value of X? Doesn't matter? What if there are be other constraints on X?

As an aside, I suppose we already have a limited form of coercions for overloaded literals. That case is a lot simpler though, since coercions are triggered by syntax.

[andreasabel]

Well, just arbitrary coercions wouldn't work. I guess we would have similar restrictions as for instances, that the types you coerce between must be named types.