Finite sets

[winterkoninkje]

So, I just encountered a most delicious type the other day:

class Finite a where
    assemble :: Applicative f => (a -> f b) -> f (a -> b)

What's so nice about it is that the only way you can implement it is if the type a is in fact finite. (But see the notes.) So the questions are:

• Can you see why?
• Can you figure out how to implement it for some chosen finite type?
• Can you figure out how to implement it in general, given a list of all the values? (you may assume Eq a for this one)
• Can you figure out how to get a list of all the values, given some arbitrary implementation of assemble?

A trivial note: Well, of course you can implement anything in Haskell by using undefined or equivalent. For the sake of these problems, assume you're constrained to use only fully-defined functions.

A big note, also a hint perhaps: And really, there's nothing here that truly forces the type to be finite. In order to get some real logical guarantees, you should assume you're in a total language (preferably a provably-total language), and you should use the following dependent type instead:

class Finite a where
    assemble :: Applicative f => ((x::a) -> f (b x)) -> f ((x::a) -> b x)

Comments

[https://www.google.com/accounts/o8/id?id=AItOawm1TLhBIxtjGvZl0SEwUGP3KGjyQByPLas]

Note that this is exactly the type signature for sequenceA for a hypothetical ((->) a)-instance of Traversable.

My solution for assemble when given [a]:


assemble values f = select <$> traverse (\x -> fmap (\y -> (x,y)) (f x)) values
where select l x = fromJust (lookup x l)


I haven't figured out how to get [a] when given assemble.

[https://www.google.com/accounts/o8/id?id=AItOawm1TLhBIxtjGvZl0SEwUGP3KGjyQByPLas]

Looks like something ate my whitespace. And I should probably have renamed assemble to assemble' in order to differentiate between the function that is a class member, and the function I defined in order to help instantiating that class.

Having experimented with my assemble' definition, I don't think it is possible to get Finite a => [a] given just the definition of assemble. In particular, I have not found a way to make the following hold:

exists f. forall values. valuesOf (assemble' values) == values

That is, a definition function valuesOf that takes the definition of assemble and produces a list of all values can't retrieve the values given to assemble'. As far as I can tell, with my assemble' definition, differentiating between assemble' [1,2,3] and assemble' [1,2,4] doesn't seem possible.

The amount of values of that type can be recovered, though. Pass \x -> [x,x] as argument to assemble. The length of the resulting list will be 2^amount. If you pass \x -> [x,x,x], the resulting list will have 3^amount elements.

[winterkoninkje]

For your enjoyment:

domain :: Finite a => [a]
domain = toList . execWriter . assemble $ tell . return

Where toList is from DList and brings the runtime down to O(n) instead of O(n^2) due to the writer monad always appending to the right.

[https://www.google.com/accounts/o8/id?id=AItOawm1TLhBIxtjGvZl0SEwUGP3KGjyQByPLas]

Oooh, using Writer. That's clever, and works. Thanks!