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?

CodePudding user response：

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

CodePudding user response：

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.