# What are some good (bad) examples of "green slime"?

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

• Where is this "green slime" originated/referenced? Jul 19 at 23:48
• It's a McBride-ism. Green is/was the color of functions in his syntax highlighter, and the "Don't touch the green slime!" rule of thumb is that you should avoid defined functions in data type indices: personal.cis.strath.ac.uk/conor.mcbride/PolyTest.pdf Jul 20 at 9:55
• Jul 20 at 9:56
• I blame Conor McBride for this question. He should answer it. Jul 21 at 19:59

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.

• 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. Jul 29 at 4:12
• 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. Jul 30 at 19:34
• 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. Aug 1 at 15:05