Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Understanding the Fix datatype in Haskell

In this article about the Free Monads in Haskell we are given a Toy datatype defined by:

data Toy b next =
    Output b next
  | Bell next
  | Done

Fix is defined as follows:

data Fix f = Fix (f (Fix f))

Which allows to nest Toy expressions by preserving a common type:

Fix (Output 'A' (Fix Done))              :: Fix (Toy Char)
Fix (Bell (Fix (Output 'A' (Fix Done)))) :: Fix (Toy Char)

I understand how fixed points work for regular functions but I'm failing to see how the types are reduced in here. Which are the steps the compiler follows to evaluate the type of the expressions?

like image 666
Jesuspc Avatar asked Aug 28 '17 09:08

Jesuspc


People also ask

How do you define a data type in Haskell?

The Data Keyword and Constructors In general, we define a new data type by using the data keyword, followed by the name of the type we're defining. The type has to begin with a capital letter to distinguish it from normal expression names. To start defining our type, we must provide a constructor.

How do types work in Haskell?

In Haskell, every statement is considered as a mathematical expression and the category of this expression is called as a Type. You can say that "Type" is the data type of the expression used at compile time.

What is fix Haskell?

fix will find a fixed point of fact' , i.e. the function f such that f == fact' f . But let's expand what this means: f = fact' f = \n -> if n == 0 then 1 else n * f (n-1) All we did was substitute rec for f in the definition of fact' . But this looks exactly like a recursive definition of a factorial function!

How do you read type in Haskell?

In Haskell read function is used to deal with strings, if you want to parse any string to any particular type than we can use read function from the Haskell programming. In Haskell read function is the in built function, that means we do not require to include or install any dependency for it, we can use it directly.


1 Answers

I'll make a more familiar, simpler type using Fix to see if you'll understand it.

Here's the list type in a normal recursive definition:

data List a = Nil | Cons a (List a)

Now, thinking back at how we use fix for functions, we know that we have to pass the function to itself as an argument. In fact, since List is recursive, we can write a simpler nonrecursive datatype like so:

data Cons a recur = Nil | Cons a recur

Can you see how this is similar to, say, the function f a recur = 1 + recur a? In the same way that fix would pass f as an argument to itself, Fix passes Cons as an argument to itself. Let's inspect the definitions of fix and Fix side-by-side:

fix :: (p -> p) -> p
fix f = f (fix f)

-- Fix :: (* -> *) -> *
newtype Fix f = Fix {nextFix :: f (Fix f)}

If you ignore the fluff of the constructor names and so on, you'll see that these are essentially exactly the same definition!


For the example of the Toy datatype, one could just define it recursively like so:

data Toy a = Output a (Toy a) | Bell (Toy a) | Done

However, we could use Fix to pass itself into itself, replacing all instances of Toy a with a second type parameter:

data ToyStep a recur = OutputS a recur | BellS recur | DoneS

so, we can then just use Fix (ToyStep a), which will be equivalent to Toy a, albeit in a different form. In fact, let's demonstrate them to be equivalent:

toyToStep :: Toy a -> Fix (ToyStep a)
toyToStep (Output a next) = Fix (OutputS a (toyToStep next))
toyToStep (Bell next) = Fix (BellS (toyToStep next))
toyToStep Done = Fix DoneS

stepToToy :: Fix (ToyStep a) -> Toy a
stepToToy (Fix (OutputS a next)) = Output a (stepToToy next)
stepToToy (Fix (BellS next)) = Bell (stepToToy next)
stepToToy (Fix (DoneS)) = DoneS

You might be wondering, "Why do this?" Well usually, there's not much reason to do this. However, defining these sort of simplified versions of datatypes actually allow you to make quite expressive functions. Here's an example:

unwrap :: Functor f => (f k -> k) -> Fix f -> k
unwrap f n = f (fmap (unwrap f) n)

This is really an incredible function! It surprised me when I first saw it! Here's an example using the Cons datatype we made earlier, assuming we made a Functor instance:

getLength :: Cons a Int -> Int
getLength Nil = 0
getLength (Cons _ len) = len + 1

length :: Fix (Cons a) -> Int
length = unwrap getLength

This essentially is fix for free, given that we use Fix on whatever datatype we use!

Let's now imagine a function, given that ToyStep a is a functor instance, that simply collects all the OutputSs into a list, like so:

getOutputs :: ToyStep a [a] -> [a]
getOutputs (OutputS a as) = a : as
getOutputs (BellS as) = as
getOutputs DoneS = []

outputs :: Fix (ToyStep a) -> [a]
outputs = unwrap getOutputs

This is the power of using Fix rather than having your own datatype: generality.

like image 89
AJF Avatar answered Oct 03 '22 19:10

AJF