Finite Types

Jul 31, 2011 20:14


So if a type has a finite number of values, it's possible to make it an instance of this type, which you can find in my countable package:

class (Eq a) => Finite a where { allValues :: [a]; assemble :: (Applicative f) => (a -> f r) -> f (a -> r); };

I hope allValues is straightforward. But assemble is more interesting. The basic idea is that if a is finite, then (a -> r) is a finite number of rs. For example, (Bool -> r) is a pair of rs, i.e. it's isomorphic to (r,r). So assemble is just a generalisation of these:

assemble2 :: (Applicative f) => (f r,f r) -> f (r,r); assemble3 :: (Applicative f) => (f r,f r,f r) -> f (r,r,r); ...

Now it is possible to generate assemble from allValues, and I have that as the default implementation in the Finite class. But it's slow and ugly, so where feasible I try to write them by hand. Here are some examples (of course relying on (Finite a,Finite b)):

assemble afb = liftA2 (\f t x -> if x then t else f) (afb False) (afb True); // Bool assemble eabfr = liftA2 either (assemble (eabfr . Left)) (assemble (eabfr . Right)); // Either a b assemble abfr = fmap (\abr (a,b) -> abr a b) (assemble (\a -> assemble (\b -> abfr (a,b)))); // (a,b)

I've spent much of this weekend trying to write one for (a -> b). I finally figured it out, and it involves this type:

data Exp a b f r = Closed (f r) | Open a (Exp a b f (b -> r)); runExp :: (Functor f) => Exp a b f r -> f ((a -> b) -> r);

The type can be made an instance of Applicative, and runExp pulls out what you need. Once you work in that, everything falls out. I think. I mean, it compiles, so it must be correct... But the odd thing is, I've written this type before, to represent lambda-expressions for a Scheme interpreter:

data SymbolLambdaFunctorExpression sym val f a = Closed (f a) | Open sym (SymbolLambdaFunctorExpression sym val f (val -> a));

Very odd. I'm not sure what the connection is, though the equivalent of runExp would evaluate an expression using a symbol-table.

software, maths

Previous post Next post
Up