I'm reading Thinking with Types, chapter4 has a question that:

type family AlwaysUnit a where
    AlwaysUnit a = ()

{- which a is ambiguous type? -}
AlwaysUnit a -> a
b -> AlwaysUnit a -> b
Show a => AlwaysUnit a -> String 

I know that Show a => AlwaysUnit a -> String has ambiguous type, but I want to know why AlwaysUnit a -> a has no ambiguous type? I cann't implement AlwaysUnit a -> a this type signature into a function.

CodePudding user response：

type aliases (and type family aliases by extension) do not create new types. They literally alias to the thing on the right hand side. In your case, there's only one branch in the type family, and it matches all types, so it will always be taken. So AlwaysUnit a is always equal to (). Not isomorphic, not sort-of-similar, but equal. That is, these three types

AlwaysUnit a -> a
b -> AlwaysUnit a -> b
Show a => AlwaysUnit a -> String

are entirely equal (again, not isomorphic, but a very strong form of equality) to these three

() -> a
b -> () -> b
Show a => () -> String

In the first example, we still have an a, so it's not ambiguous. In the second example, a is completely eliminated, so it's as though it wasn't there in the first place. Haskell is happy to quietly ignore the "unused" variable. In the third example, however, we have a variable a that is used in the constraint (the thing on the left of the =>) but not in the type proper. That's going to create a problem whenever we try to call that function, and short of TypeApplications I don't think there's a good way to resolve that conflict.

Note that things would be more complicated if AlwaysUnit had multiple cases or did some pattern matching against its type. You can end up in a situation where none of the cases match or where GHC can't decide whether the case should match or not, and it will refuse to simplify. In that case, you'll end up with an AlwaysUnit a that doesn't simplify in your type.

I cann't implement AlwaysUnit a -> a this type signature into a function.

That's a good intuition, but there are a couple of problems. First, you can always implement any function in Haskell.

f :: AlwaysUnit a -> a
f _ = undefined

So, if we're allowing bottom types, then every type in Haskell is inhabited. And even if we're not allowing bottom types, then "can I implement this function" and "is the type ambiguous" are entirely different questions. For instance, I can't implement a function of type Int -> Void without resorting to bottom types, since Int is clearly inhabited and Void is clearly not. But it's not an ambiguous type. It's a perfectly well-defined but empty function type.

CodePudding user response：

Of course, you can't implement AlwaysUnit a -> a when a is an unbound type variable (without cheating by using ⊥). But that's not what the question asks. Ambiguous types are asking, if the compiler encounters an expression with this type, can it infer a type for a from context?

Suppose we have

exercise1 :: AlwaysUnit a -> a
exercise1 = undefined

main = putStrLn $ exercise1 ()

Can you tell what type has been chosen for a at this call site? Yes, because putStrLn demands a String, we must have a ~ String. Thus, the a type variable in the definition of exercise1 is not ambiguous.

For the other two exercises, there is no context you could put those types into that would allow you to infer the type of a. In exercise 2, that's fine - nobody needs to know what a is to use that function. But in exercise 3, a is needed to resolve the Show constraint, so it is ambiguous.