Phantom arguments [Re: [Agda] Agdas constraint solver too eager?!]

[Andreas Abel]

On 08.09.12 9:36 PM, James Deikun wrote:
> On Fri, 2012-09-07 at 15:13 +0200, Andreas Abel wrote:
>>     1. Go the 'semantic path' for data type parameters, allowing Agda to
>>        recognize them as unused.  That will make certain phantom tricks
>>        impossible.
>>        I am a bit confused, since I thought by getting rid of injective
>>        type constructors we had already gotten there, but it seems not.
>>
>>     2. Go the 'syntactic path' for data type parameters, considering them
>>        never as unused, to allow phantom tricks.
>>        The relationship to injective type constructors should be
>>        clarified then.
>>
>> I am tending towards 1., but people using phantoms should speak up to
>> discuss whether they are essential and whether they could sustain when
>> going 1.

I decided to stick with 2. for now, being conservative.

> I feel this change would cause a lot of problems for the categories
> library, which often uses phantom or semi-phantom record type parameters
> to keep track of things like domains and codomains.  There are already
> problems coming from the way irrelevant arguments are inferred, as you
> may remember, but this sort of thing could make them much worse.
>
> I can't be sure of course; perhaps you could try testing the categories
> library ( http://github.com/copumpkin/categories/ ) against your
> prospective implementation if you have the opportunity.

Thanks for the pointer.  This is a useful test-suite, especially for 
stuff like irrelevance.  I ran your contribution through Agda after my 
changes.  It turnes out your library compiles just fine (after I fixed 
some bugs in the Agda development version.)

Here is a tiny random observation about Categories.Support.SetoidPi. 
You can avoid making resp-per' irrelevant if you make the two 
`equiv'-arguments to resp-per irrelevant (which they are, but they have 
not been declared as such).  The new code would be the following 
re-dotting of the old code:

resp-per : ∀ {c ℓ} {C₁ C₂ : Set c} {_≈₁_ : B.Rel C₁ ℓ} {_≈₂_ : B.Rel C₂ ℓ}
   → .{equiv₁ : B.IsEquivalence _≈₁_} .{equiv₂ : B.IsEquivalence _≈₂_}
   → C₁ ≡ C₂
   → _≈₁_ ≅ _≈₂_
   → _≡_ {A = Setoid c ℓ}
         record {Carrier = C₁; _≈_ = _≈₁_; isEquivalence = equiv₁}
         record {Carrier = C₂; _≈_ = _≈₂_; isEquivalence = equiv₂}
resp-per _≡_.refl ≅-refl = _≡_.refl

resp-per′ : ∀ {c ℓ} (S T : Setoid c ℓ)
    → (Carrier₀ S ≡ Carrier₀ T)
    → (Setoid._≈_ S ≅ Setoid._≈_ T)
    → S ≡ T
resp-per′ S T = resp-per {equiv₁ = Setoid.isEquivalence S}
                          {equiv₂ = Setoid.isEquivalence T}

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/