6
$\begingroup$

I know what this roughly is. But when I'm explaining to a friend, I have trouble pulling out examples from my head. Are there any minimal working examples (maybe "minimal non-working examples" is a more appropriate name) for "green slime"?

$\endgroup$
4

1 Answer 1

4
$\begingroup$

If all you want is a very simple example, it's pretty easy to build one. Here's one simplified from a question on the Agda zulip:

open import Data.Bool

variable b c : Bool

data P : Bool → Set where
  base : P false
  slime : P b → P c → P (b ∨ c)

f : P false → _
f p = {!p!}

If you try to split on $p$, Agda will say it doesn't know whether there should be a $\sf slime$ case. This is because it doesn't know how to solve the unification problem $b ∨ c = \mathsf{false}$.

You might think that Agda could be improved to actually notice that in this case, there are unique solutions for $b$ and $c$, so the $\sf slime$ case could be allowed. However, you could then use $∧$ instead of $∨$ (or $\sf true$ instead of $\sf false$) to cause there to be multiple solutions, so matching on $\sf slime$ as a singular case no longer makes sense.

You might then think that you could do something like:

f (slime {b = false} {c = false} q r) = ...
...

where in the $∧$ case you could enumerate all the valid cases. However, Agda at least does not allow this either. I'm unsure how workable this would actually be. It seems simple in this case, but I would be unsurprised if you can encode some undecidable problem this way. So probably the best you can hope for is heuristic.

$\endgroup$
3
  • 1
    $\begingroup$ It seems to me like this is just an artifact of thinking of pattern-matching as the fundamental operation instead of eliminators / induction principles. When you define an indexed datatype, the eliminator requires its motive to be general over all indices. So of course you can't define a function by induction on P false; that would be like trying to prove something about 3 by ordinary induction on natural numbers. It doesn't mean there's anything wrong with the indexed datatype, just that you have to use the appropriate eliminator for it. $\endgroup$ Jul 29 at 4:12
  • $\begingroup$ The context of these sort of guidelines is making programming with more precise types palatable to 'working' programmers. (Dependent) pattern matching fits into this because it is comparable to actual practical languages. Plain MLTT is not, even if it is considered "fundamental." It doesn't really matter how, "you need to do extra work," is justified foundationally. Guidelines on how to make (ensured) correct programs comparably natural to write as ordinary programs mean people might actually write the former. Methods that lead to extra obstacles mean people probably just won't bother. $\endgroup$
    – Dan Doel
    Jul 30 at 19:34
  • $\begingroup$ I think I didn't express mysellf well. I didn't mean to say that everyone should program with eliminators instead of pattern-matching, just that the theoretical justification of pattern-matching is in terms of eliminators. So when trying to understand or explain why it doesn't work to split on p : P false, talking about induction provides a more solid explanation than "Agda can't guess", as well as an alternative solution: if you don't want to avoid functions in indices, you can instead just make sure all your pattern-matches are general over the indices. $\endgroup$ Aug 1 at 15:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.