Phantom arguments in functions [Re: [Agda] another possible without-K problem]

[Guillaume Brunerie]

Thanks, that’s much simpler.
But using instance arguments for that is indeed overkill.
In the HoTT-Agda library (branch 2.0) I implemented the version with
an instance argument and tried to compile the proof of pi_1(S^1)=Z.
Then either Agda starts eating all the RAM (if I add the instance
argument only for the dependent elimination rule) or I get an internal
error (if I add the instance argument for both the dependent and
nondependent elimination rules) :-(
But Dan’s version without the instance argument works without trouble.

Guillaume

2013/7/11 Andreas Abel <andreas.abel at ifi.lmu.de>:
> Dan, Guillaume,
>
> Here is a revised showcase for the phantom trick, following your improvement
> suggestions.
>
> * There is not need for a Phantom record type, one can just take a
> parametrized unit type.
>
> * The phantom argument can be found by instance search.
>   Of course, one can define a wrapper that supplies the phantom argument,
> like Dan did below.
>
> Hmm, since people need to work around the unused argument analysis, I wonder
> whether it was good to add it.  I wanted definitional equality to be a bit
> more "extensional".  But it seems the workaround is only needed in another
> workaround (the absence of HITs).  ;-)
>
> Cheers, Andreas
>
>
>
> import Common.Level
> open import Common.Equality
>
> data Phantom {A : Set}(a : A) : Set where
>   phantom : Phantom a
>
>
> postulate
>   A      : Set
>   a      : A
>   Unused : Set
>   u1 u2  : Unused
>
> data Unit : Set where
>   unit : Unit
>
> bla : (u : Unused) → Unit → A
> bla u unit = a
>
> same : {x : Unit} → bla u1 x ≡ bla u2 x
> same = refl
>
> fool : (u : Unused){{z : Phantom u}} → Unit → A
> fool u {{phantom}} unit = a
>
> same? : ∀ {x : Unit} → fool u1 x ≡ fool u2 x
> same? = refl
>
> -- ERROR:
> -- u1 != u2 of type Unused
> -- when checking that the expression refl has type
> -- fool u1 .x ≡ fool u2 .x
>
>
>
> On 10.07.13 9:09 PM, Dan Licata wrote:
>>
>> Hi Andreas, Guillaume,
>>
>> Andreas, thanks for the suggestion!
>>
>> Guillaume, unless I'm mistaken, or things have changed since 2.3.2.1, I
>> think there
>> is a simpler way to avoid the annoyance of the phantom argument:
>>
>> - To make an unused argument used, you need to match on a "phantom"
>>    argument indexed by that argument.  (I.e. it's important that
>>    the unit in Andreas's code is a data, not a record)
>>
>> - But it's OK if the function is always called on the canonical
>>    inhabitant of the type you're matching on---you don't need to quantify
>>    over variable phantoms like Andreas is doing in his example.
>
>
> Yes, of course, that is simpler & better.
>
>
>>    This is important for getting the right definitional behavior, as
>>    otherwise the match on the phantom would block reduction.
>>
>> So the trick can be hidden in the implementation of the HIT, without
>> changing the external interface.
>>
>> For example, the following implementation of a higher inductive type
>> works for me in 2.3.2.1. (Guillaume, does it still work in the
>> development version?)
>>
>> Andreas, perhaps you could confirm that this is reasonable, given the
>> meaning of the unused argument check?
>
>
> Yes, this is reasonable.
>
>
>> Also: does anyone know if there is a nice way to install and switch
>> between multiple versions of Agda?
>> How would I have 2.3.2.1 from cabal and the devel version installed
>> simultaneously?
>>
>> -Dan
>>
>> ----------------------------------------------------------------------
>>
>> {-# OPTIONS --type-in-type --without-K #-}
>>
>> open import lib.Prelude --  ≃ and id are the identity type and refl; Type
>> is Set
>>
>> module misc.Phantom where
>>
>> data Unit⁺ : Type where
>>    <>⁺ : Unit⁺
>>
>> record Phantom {A : Type}(a : A) : Type where
>>    constructor phantom
>>    field
>>      match : Unit⁺
>>
>> module S where
>>        private
>>          data S¹' : Type where
>>            Base : S¹'
>>
>>        S¹ : Type
>>        S¹ = S¹'
>>
>>        base : S¹
>>        base = Base
>>
>>        postulate {- HoTT Axiom -}
>>          loop : Path base base
>>
>>        S¹-rec' : {C : Type}
>>               -> (c : C)
>>               -> (p : c ≃ C) (_ : Phantom p)
>>               -> S¹ -> C
>>        S¹-rec' c p (Phantom.phantom <>⁺) Base = c
>>
>>        S¹-rec : {C : Type}
>>               -> (c : C)
>>               -> (p : c ≃ c)
>>               -> S¹ -> C
>>        S¹-rec c p = S¹-rec' c p (Phantom.phantom <>⁺)
>>
>> {- correctly fails:
>>
>> p != q of type Id c c
>> when checking that the expression id has type
>> Id (S.rec c p) (S.rec c q)
>>
>> test : {C : Type}
>>       -> (c : C)
>>       -> (p q : c ≃ c)
>>       → S.S¹-rec c p ≃ S.S¹-rec c q
>> test c p q = id
>> -}
>>
>> -- still get definitional computation on points
>>
>> test' : {C : Type}
>>       -> (c : C)
>>       -> (p : c ≃ c)
>>       → S.S¹-rec c p S.base ≃ c
>> test' c p = id
>>
>>
>>
>> On Jul10, Guillaume Brunerie wrote:
>>>
>>> Thanks for the workaround!
>>> It’s not optimal though, you have to give the silly [z] argument
>>> everytime you use [fool] which is a bit annoying.
>>> But this is easy to fix by making the argument [z] of [fool] an
>>> instance argument instead of an implicit argument and by putting
>>> somewhere in the context the following definition:
>>>
>>> inhab-Phantom : {A : Set} {a : A} -> Phantom a Unit
>>> inhab-Phantom = phantom unit
>>>
>>> Then you can use [fool] just as you use [bla]:
>>>
>>> same? : {x : Unit} → fool u1 x ≡ fool u2 x
>>> same? = refl
>>>
>>> gives the expected error.
>>>
>>> Guillaume
>>>
>>> 2013/7/10 Andreas Abel <andreas.abel at ifi.lmu.de>:
>>>>
>>>> On 10.07.2013 16:54, Dan Licata wrote:
>>>>>
>>>>>
>>>>> Also, related to implementing higher inductives, but not to without-K:
>>>>> is there a way to turn off/defeat the unused arguments analysis that is
>>>>> new in 2.3.2.1?  It breaks some of the things I'm doing: I want a
>>>>> function with a "phantom" parameter, where different values of the
>>>>> phantom parameter do not automatically get equated.
>>>>
>>>>
>>>>
>>>> Data and record types still have phantom arguments, which can be
>>>> exploited.
>>>>
>>>> Would this workaround help you?
>>>>
>>>> import Common.Level
>>>> open import Common.Equality
>>>>
>>>> record Phantom {A : Set}(a : A)(B : Set) : Set where
>>>>    constructor phantom
>>>>    field
>>>>      thePhantom : B
>>>> open Phantom
>>>>
>>>> postulate
>>>>    A      : Set
>>>>    a      : A
>>>>    Unused : Set
>>>>    u1 u2  : Unused
>>>>
>>>> data Unit : Set where
>>>>    unit : Unit
>>>>
>>>> bla : (u : Unused) → Unit → A
>>>> bla u unit = a
>>>>
>>>> same : {x : Unit} → bla u1 x ≡ bla u2 x
>>>> same = refl
>>>>
>>>> fool : (u : Unused){z : Phantom u Unit} → Unit  → A
>>>> fool u {phantom unit} unit = a
>>>>
>>>> same? : ∀ {x : Unit}{y z} → fool u1 {y} x ≡ fool u2 {z} x
>>>> same? = refl
>>>>
>>>> -- ERROR:
>>>> -- u1 != u2 of type Unused
>>>> -- when checking that the expression refl has type
>>>> -- fool u1 .x ≡ fool u2 .x
>>>>
>>>>
>
> --
> 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/