Take this code snippet:

-- a type family for which I won't define any instances
type family EmptyTypeFamily t

-- 1. this type doesn't exist, since there's no `instance EmptyTypeFamily ()`
type NotAType = EmptyTypeFamily ()

-- 2. this value has a type that doesn't exist
untypedValue :: NotAType
untypedValue = undefined

main :: IO ()
main = do
  -- 3. the value with no type can be used in expressions
  return untypedValue
  return . id . fix $ \x -> untypedValue
  
  -- ERROR, finally! No instance for `Show (EmptyTypeFamily ())`
  print untypedValue

I find it quite counter intuitive that I can name a stuck application of a type family (1) and even define values for it (2) and use them in expressions (3). Of course I can't define any typeclass instances for it, since the type doesn't even exist. But shouldn't I get an error just by naming that non-type, let alone using it? This makes it harder to detect issues in my code. I read the GHC doc, which mentions "stuck" twice, but doesn't answer my question.

What's the reason why Haskell treats EmptyTypeFamily () as a valid type for which you can even define values and whatnot, when it isn't?

CodePudding user response：

As chi remarked: it's not quite accurate to say your type family is empty, rather it merely happens to not contain any yet-known instances.
But I think that's missing the point of the question, so let's discuss instead the type family

type family EmptyTypeFamily t where {}

This one really is empty: you can't write any instances for it.

Still, this causes exactly the same behaviour as you observed. Why?

Well, what GHC does with types during compilation is in some ways similar to how we're dealing with values in all Haskell programs: lazy evaluation and pattern matching. It's well known how the program

f :: Int -> Int
f _ = 624

main :: IO ()
main = print $ f undefined

runs without problems, even though it “evaluates” undefined as the argument to f. It's ok because f doesn't actually need to know anything about its argument.

Similarly, if you write return untypedValue, then the type checker doesn't need to know anything about EmptyTypeFamily () – it just treats it as an abstract entity. It can even unify different type variables to EmptyTypeFamily (). This only requires the assumption that, whatever EmptyTypeFamily is under the hood, it must certainly be deterministic. That much is guaranteed, because the compiler would complain if you wrote two conflicting instances for it.

So, as long as you only use untypedValue with unconstraint-polymorphic functions, it simply doesn't matter that its type doesn't actually exist, because it never needs to be evaluated any further.

In other words, NotAType is purely symbolic. It's a bit like in maths, you can write a theorem starting with “let S be a set and x ∈ S, then bla bla” without actually pinning down what this set is or a value for x.

That changes only as you require additional constraints, like unifying it with a concrete type

f :: Int -> Int
f x = x   1

main = print $ f untypedValue

    • Couldn't match type ‘EmptyTypeFamily ()’ with ‘Int’
      Expected type: Int
        Actual type: NotAType
    • In the first argument of ‘f’, namely ‘untypedValue’

...or, as you observed, use typeclass methods on it. In each case, the compiler has to start with performing an actual pattern match on the type-level value EmptyTypeFamily (). Well, in fact it's a more general process: what the compiler keeps track of are rather propositions. It has a database of knowledge that such and such types are equal, and such and such types match such and such class, and in this case GHC just determines that it doesn't have information which would allow deciding on any known Show instance.

Note that it is actually possible to have a hypothetical context in which that information is available, however nonsensical that is:

{-# LANGUAGE RankNTypes, FlexibleContexts #-}

hypothetically :: (Show NotAType => r) -> ()
hypothetically _ = ()

main = return $ hypothetically (print untypedValue)

In this case, responsibility for proving Show NotAType is deferred to the implementation of hypothetically. As the compiler tackles print untypedValue it just browses through the context and sees that Show NotAType will be proved by whatever code eventually uses the argument to hypothetically. ...Which of course never happens, but the compiler doesn't worry about that when typechecking main.

This, in the maths analogy, is like writing a proof starting with “let x ∈ ℝ such that x² = -1...” – this is perfectly valid and allows you to prove exciting things. Only, nobody will be able to use the theorem for computing something, because there exists no real number with the required property.

CodePudding user response：

since there's no instance EmptyTypeFamily ()

There is no such instance, yet.

When compiling a module, we do not (yet) know whether another module actually defines such an instance, hence we must be ready for that to happen. This is called the "open world assumption".

Haskell is meant to allow for separate compilation, i.e. compiling each module individually. Also, Haskell allows each module to add arbitrary instances. Coherently, we can never be sure an instance does not exist during compilation.

To be pedantic, Haskell also allows closed type families, which can not be extended in such a way, but IIRC it handles stuck close type families like stuck open ones. Perhaps it should reject those, after all. In closed type families one can however force rejection by adding an explicit TypeError ".." final case in the definition of the closed type family.