Quelklef

milk consumer

girly but not a girl

name-color: #C09


Quelklef
@Quelklef

is that the following instance exists (and is not just undefined):

-- Infinite sequences
data InfSeq a = InfSeq a (InfSeq a)

-- Crazy instance
instance Eq y => Eq (InfSeq Bool -> y)

Quelklef
@Quelklef

technically, this fact boils down to "computable functions are continuous and the cantor space InfSeq Bool is compact". but that's nerd shit

conceptually this boils down to the fact that due to properties of computability, a value of type InfSeq Bool -> y necessarily only observes a finite number of elements from the given InfSeq Bool. Hence, to compare two values of type InfSeq Bool we need only compare how they act on some finite subset of InfSeq Bool.

Unfortunately, actually doing this is extremely subtle, and even after multiple reviews of this topic I don't fully understand the details.

(I first learned about this from a blog post from Martin Escardo. Also see my notes on the topic, which contain an implementation of the algorithm that is--in my opinion--simpler)


You must log in to comment.