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?

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.

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

Missing some laws

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

Without some laws this type doesn't tell us anything about the finiteness of a type (as far as I can tell).

import Control.Applicative

assemble1 :: Applicative f => a -> (a -> f b) -> f (a -> b)
assemble1 a f = fmap const (f a)

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

instance Assemble Integer where
  assemble = assemble1 0

As long as we have one element of the type we can implement the rest, finite or not. Perhaps there were other constraints that an implementation should satisfy.

Re: Missing some laws

[winterkoninkje]

That's exactly what I mentioned in the second note. Of course, even though the collections of all values of a given type may not be finite; this encoding does give a specification of a finite subset of values from that type. Thus, it can be considered an alternative to strict lists for ensuring finiteness of a collection.

Of course, as an attempt to enumerate all values in the type, your instance isn't morally correct. In this case, the morality in question can be enforced with dependent types. Can you find any way to break the dependent version? (nontermination doesn't count.)

[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!