winterkoninkje: shadowcrane (clean) (Default)

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)

Anonymous( )Anonymous This account has disabled anonymous posting.
OpenID( )OpenID You can comment on this post while signed in with an account from many other sites, once you have confirmed your email address. Sign in using OpenID.
Account name:
If you don't have an account you can create one now.
HTML doesn't work in the subject.


If you are unable to use this captcha for any reason, please contact us by email at

Notice: This account is set to log the IP addresses of everyone who comments.
Links will be displayed as unclickable URLs to help prevent spam.

June 2017

18192021 222324


Page generated 25 Jul 2017 06:32 am
Powered by Dreamwidth Studios