2

I didn't have any problems understanding how fix function works in Haskell, but I just can't wrap my head around Fix data type. I believe I get the idea behind it, but I just can't understand how Fix data type definition works under the hood. So, Fix is defined like this:

newtype Fix f = Fix { unfix :: f (Fix f) }

The way I parse this definition in my head is that Fix as a data type is a record with one field, unfix, which has a type of f (Fix f). So, in order to construct this type, you use Fix type constructor with an argument in form of f (Fix f), correct?

If my understanding so far is indeed correct, then I need an explanation why the following is accepted by the compiler:

data T a = Dummy t = Fix Dummy

Here, the argument to Fix is not in the form of f (Fix f), but the compiler doesn't reject the code, but why? f (Fix f) seems like two terms thingy to me, one term for f and another for Fix f, but Dummy is just one term, so for me the code above should not work for that reason alone. Apparently, the compiler does something under the hood that I'm missing in my reasoning and this is what I need help with.

And the bonus question is why Fix 1 is also accepted by the compiler and what's going on in this case?

Improve this question
2
  • 4
    Generally speaking, what type does the expression Dummy have? Commented May 14, 2022 at 15:19
  • Fix has a single field, so there's only supposed to be a single term. That term's type has to be of the form f (Fix f), not the term itself. (Although f (Fix f) is also a single type-level expression, not "two terms"; it's f applied to Fix f, not f and then a separate Fix f) Commented May 14, 2022 at 16:33

2 Answers 2

Reset to default
4 
data T a = Dummy t = Fix Dummy

Here, the argument to Fix is not in the form of f (Fix f), but the compiler doesn't reject the code, but why?

Oh, but it is in the form f (Fix f)! Check this out:

 Dummy :: T a Dummy :: a ~ Fix T => T a Dummy :: T (Fix T) Dummy :: f ~ T => f (Fix f)

And the bonus question is why Fix 1 is also accepted by the compiler and what's going on in this case?

Number literals are polymorphic. So 1 :: Num a => a. There aren't any instances of the form instance Num (F X) in the Prelude, but there's nothing stopping somebody from later defining one. As mentioned by Noughtmare, an example of this in the base libraries is instance Num a => Num (Const a). So:

Fix :: f (Fix f) -> Fix f 1 :: Num a => a 1 :: Num (f (Fix f)) => f (Fix f) Fix 1 :: Num (f (Fix f)) => Fix f
Improve this answer
Sign up to request clarification or add additional context in comments.

1 Comment

For Fix 1 you can pick the concrete type f ~ Const Int.
0

Dummy has type T a for any choice of type a :: Type, and Fix has type f (Fix f) -> Fix f for any choice of type constructor f :: Type -> Type. In order to be well-typed, in the expression Fix Dummy, the compiler therefore needs to choose a and f so that the type of Dummy matches the input type of Fix, namely, T a must equal f (Fix f).

All you’re missing is that T a = f (Fix f) implies T = f and a = Fix f. In this case, that means we’re applying Fix :: T (Fix T) -> Fix T to Dummy :: T (Fix T).

The language is designed so that, by default, the compiler can assume the equality constraint (m x ~ n y) means (m ~ n, x ~ y), because m and n must ultimately stand for concrete “matchable” type constructors like Maybe or Either String, which can’t behave differently based on the choice of x or y.

Back to your code, this can also be written using the TypeApplications language option, as Fix @T (Dummy @(Fix T)). That is, you can explicitly pass the type argument T for the parameter f, and Fix T for a.

Improve this answer

Comments

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.