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

[Andreas Abel]

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/