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"?
$\begingroup$
$\endgroup$
4
-
4$\begingroup$ Where is this "green slime" originated/referenced? $\endgroup$– ice1000 ♦Commented Jul 19, 2022 at 23:48
-
5$\begingroup$ 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 $\endgroup$– Li-yao XiaCommented Jul 20, 2022 at 9:55
-
2$\begingroup$ Relevant: doisinkidney.com/posts/2018-09-20-agda-tips.html $\endgroup$– Li-yao XiaCommented Jul 20, 2022 at 9:56
-
8$\begingroup$ I blame Conor McBride for this question. He should answer it. $\endgroup$– Andrej BauerCommented Jul 21, 2022 at 19:59
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
5
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.
-
3$\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 about3by 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$ Commented Jul 29, 2022 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 DoelCommented Jul 30, 2022 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$ Commented Aug 1, 2022 at 15:05 -
$\begingroup$ @MikeShulman This is sound advice, but not complete advice. As the question suggests, with dependent pattern-matching at hand, it's only green indices that cause problems – non-general constructors are also fine. To take your example, it's perfectly easy to eliminate a
Fin 3into its 3 cases, despite this not corresponding directly to an induction over all ofFin. The difference from the example in the answer is that all of the unification problems are constructor-constructor (red-red) or constructor-variable (red-purple). $\endgroup$ Commented Aug 10, 2022 at 8:39 -
$\begingroup$ @mudri Thanks for that point! Unless I misunderstand, though, that can also be explained in terms of eliminators. The standard way to prove things about special instances of an indexed datatype is to define a special motive by recursion over the base (into the universe) and then apply the eliminator. (In homotopy type theory we call this the "encode-decode" method, but it's much older than that of course.) But of course such a motive can only be defined by case analysis on constructors of the base, not arbitrary functions. $\endgroup$ Commented Aug 14, 2022 at 18:45