2

The Agda standard library provides a data type Maybe accompanied with a view Any. Then there is the property Is-just defined using Any. I found working with this type difficult as the standard library provides exactly no tooling for Any.

Thus I am looking for examples on how to work with Is-just effectively. Is there an open source project that uses it?

Alternatively, I am seeking how to put it to good use:

  • Given Is-just m and Is-nothing m, how to eliminate? Can Relation.Nullary.Negation.contradiction be used here?
  • Given a property p : ... → (mp : Is-just m) → ... → ... ≡ to-witness mp that needs to be shown inductively by p ... = {! p ... (subst Is-just m≡somethingelse mp) ... !}, the given term does not fill the hole, because it has type ... ≡ to-witness (subst Is-just m≡somethingelse mp).

Often it seems easier to work with Σ A (_≡_ m ∘ just) than Is-just m.

Helmut Grohne
  • 6,578
  • 2
  • 31
  • 67
  • 1
    Singletons approach `record Is {α} {A : Set α} (x : A) : Set where` looks nicer to me than `Σ A (_≡_ m ∘ just)`: `from-is-just : ∀ {α} {A : Set α} {x : A} -> Is (Maybe.just x) -> A; from-is-just {x = x} _ = x`. – effectfully Jun 17 '15 at 11:37
  • If there are so many alternatives to `Is-just` that work better, why is the "worst" of all, `Is-just`, part of the standard library? – Helmut Grohne Jun 17 '15 at 11:40
  • 1
    I wrote an [answer](http://stackoverflow.com/a/31105948/3237465), that elaborates one use case for `Is-just`. – effectfully Jun 29 '15 at 00:54

1 Answers1

1

Regarding your first question, it is possible to derive a contradiction from having both Is-just m and Is-nothing m in context. You can then use ⊥-elim to prove anything.

module isJust where

open import Level
open import Data.Empty
open import Data.Maybe

contradiction :
  {ℓ : Level} {A : Set ℓ} {m : Maybe A}
  (j : Is-just m) (n : Is-nothing m) → ⊥
contradiction (just _) (just pr) = pr

The second one is a bit too abstract for me to be sure whether what I'm suggesting will work but the usual strategies are to try to pattern match on the value of type Maybe A or on the proof that Is-just m.

As for using another definition of Is-just, I tend to like

open import Data.Bool

isJust : {ℓ : Level} {A : Set ℓ} (m : Maybe A) → Set
isJust m = T (is-just m)

because it computes.

gallais
  • 11,823
  • 2
  • 30
  • 63
  • Is there public example code that uses this `isJust` instead? – Helmut Grohne Jun 17 '15 at 11:18
  • 1
    Sure. For instance I defined `fromJust` for a similar `isJust` [here](https://github.com/gallais/agdARGS/blob/master/agdARGS/Data/Maybe.agda) and use it to make smart constructors [there](https://github.com/gallais/agdARGS/blob/master/agdARGS/Data/UniqueSortedList/SmartConstructors.agda#L21) – gallais Jun 19 '15 at 13:39