### Finite sets

6/1/13 20:05**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)

## Missing some laws

14/1/13 18:26 (UTC)https://www.google.com/accounts/o8/id?id=AItOawnNP5_3eRT_BuDtOzsEuFk1mSKmdeQ6mt8As 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

15/1/13 01:11 (UTC)winterkoninkjeOf 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.)

Edited 15/1/13 01:19 (UTC)## (no subject)

16/1/13 21:40 (UTC)https://www.google.com/accounts/o8/id?id=AItOawm1TLhBIxtjGvZl0SEwUGP3KGjyQByPLassequenceAfor a hypothetical((->) a)-instance of Traversable.My solution for

assemblewhen 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 givenassemble.## (no subject)

16/1/13 22:07 (UTC)https://www.google.com/accounts/o8/id?id=AItOawm1TLhBIxtjGvZl0SEwUGP3KGjyQByPLasassembletoassemble'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 getFinite a => [a]given just the definition ofassemble. 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

valuesOfthat takes the definition ofassembleand produces a list of all values can't retrieve the values given toassemble'. As far as I can tell, with myassemble'definition, differentiating betweenassemble' [1,2,3]andassemble' [1,2,4]doesn't seem possible.The amount of values of that type can be recovered, though. Pass

\x -> [x,x]as argument toassemble. The length of the resulting list will be2^amount. If you pass\x -> [x,x,x], the resulting list will have3^amountelements.## (no subject)

18/1/13 02:55 (UTC)winterkoninkje`domain :: Finite a => [a]`

domain = toList . execWriter . assemble $ tell . return

Where

`toList`

is from DList and brings the runtime down toO(n)instead ofO(n^2)due to the writer monad always appending to the right.## (no subject)

18/1/13 04:23 (UTC)https://www.google.com/accounts/o8/id?id=AItOawm1TLhBIxtjGvZl0SEwUGP3KGjyQByPLas## (no subject)

14/7/13 01:14 (UTC)http://openid-provider.appspot.com/derek.a.elkinsAll monads are applicative functors, and if you think of monads as "notions of computation" you might consider, from how you've implemented assemble, that if you were in an imperative language, you could just "save away" the values as they are applied to your supplied function and then read them out of a variable at the end. It doesn't take much from there to see that you only need to output them and that the Writer monad is sufficient.

In the second note, wren uses a dependent function type which is also known as a dependent product and this latter view is a bit more enlightening in this case. [There's a horrible terminology conflict where some people say "dependent function and dependent product" and others say "dependent product and dependent sum".] The motivation of the dependent product terminology is that the type (x :: A) -> B x can be viewed as a potentially infinite product type indexed by elements of the type A. Thus, in particular, for finite A, it is a finite product, i.e. a finite tuple. So, for example, Bool -> B is equivalent to (B, B). Applying this view to assemble, you get assemble for Bool as (Bool -> f b) -> f (Bool -> b) is the same as (f b, f b) -> f (b, b) which is an instance of liftA2 (,). Here's a different presentation of the Applicative class, as an exercise, show that it is equivalent to the normal one.

This just says that applicative functors are lax monoidal functors, i.e. they reflect (monoidal) products. In particular, this shows that they reflect all finite products. This is what allows and enforces the finiteness of the type in the Finite class. All applicative functors reflect finite products, but not all applicative functors reflect arbitrary products (i.e. functions). All implementations of assemble require implicitly or explicitly converting a function to a finite product type, exploiting that applicative functors reflect finite products and then converting the product type back into a function.