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

[Dan Licata]

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. 
  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?  

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
> >
> >
> >
> >
> >
> > 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/
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda