Lower type level values to term level in Haskell

Question

For example in the following code can I fill the hole to always compute the Nat value corresponding to the type level n parameter?

 {-# LANGUAGE DataKinds, KindSignatures, ExplicitForAll #-}
data Nat
  = Zero
  | Succ Nat

lower :: forall (n :: Nat) . Nat
lower = _

test0 = lower @Zero == Zero
test1 = lower @(Succ Zero) == Succ Zero

I tried using a type class:

class Lower (n :: Nat) where
  lower :: Nat

instance Lower Zero where
  lower = Zero

instance Lower n => Lower (Succ n) where
  lower = Succ (lower @n)

But then every time I want to use lower I need to explicitly require Lower n:

lower' :: forall (n :: Nat) . Lower n => Nat
lower' = lower @n

Answer 1

The short answer is "no".

As noted in the comments, in Haskell, type parameters are erased at runtime. What this actually means is that the runtime behavior of a function depends only on the arguments supplied for its term-level parameters, never (directly) on the arguments supplied for its type-level parameters.

Put more directly, a function is a function of its term-level parameters only, and so the value of a function application is determined by the value of the term-level arguments, irrespective of the type-level arguments. If we call the same function twice with the same term-level arguments but different type-level arguments, the two application will produce the same term-level result.

In practice, this is usually a distinction without a difference. The function:

id :: forall a. a -> a
id x = x

has runtime behavior that depends only on its term-level parameter x. If I call id True multiple times, it always produces the result True, irrespective of the type-level argument a. BUT, obviously, if the term-level argument is True, then the type-level argument is necessarily Bool, so the question of whether id True would produce the same result with different type-level arguments for parameter a is moot.

But for your example, the question is not moot. Your function:

lower :: (forall n :: Nat). Nat

must produce a value that depends only on its term-level parameters (of which there are none), and never on its type-level parameter n. Multiple calls of lower with different type-level arguments will still have the same (nullary) term-level arguments, and so the call lower must always produce the same term-level result. It is therefore impossible for lower to produce Zero for some type-level argument and Succ Zero for some other type-level argument.

A constraint is a "magical" term-level parameter. Specifically, your Lower n constraint is syntactic sugar for a newtype parameter:

newtype CLower n = CLower { lower :: Nat }

that exhibits a "coherence" property such that for each possible value for the type-level parameter n, there is only one valid term-level value of type CLower n, and Haskell will automatically supply this (only possible) term-level value wherever it is needed.

So your type-class version of lower' is roughly equivalent to:

lower' :: (forall n :: Nat). CLower n -> Nat
lower' (CLower x) = x

with the appropriate CLower n argument automatically supplied where needed.

This provides a means for the type-level parameter to come pretty close to directly determining runtime behavior. In this situation, it's still the case that lower' can only depend on its term-level parameter CLower x, but now this term-level parameter has a type (and so a value) that depends on the type-level parameter n. If you call lower' with two different type-level arguments, Haskell automatically supplies two different term-level arguments, and the result of these two lower' calls can and will return two different term-level values.

If you want to avoid a constraint and still get two different results for two different type-level arguments, you must introduce some other term-level parameter on which lower can depend. Trivially, you could write something like:

lower :: forall (n :: Nat). Int -> Nat

Now, lower has a term-level parameter (an integer), so it can produce different results for different term-level arguments:

lower 0 = Zero
lower m = Succ (lower (m-1))

This is not a very smart approach, of course, because the term-level parameter m :: Int is completely unrelated to the type-level n :: Nat parameter. If you want your term-level parameter to somehow relate to the type-level parameter n, it must have a type that depends on n, like so:

lower :: forall (n :: Nat). Something n -> Nat

and you'll need to make Something into a GADT like:

data Something n where
    SZero :: Something Zero
    SSucc :: Something n -> Something (Succ n)

so you can write a body for lower that acts on different term-level arguments that in turn have been determined by the type-level argument:

lower :: forall (n :: Nat). Something n -> Nat
lower (SZero) = Zero
lower (SSucc n) = Succ (lower n)

This isn't very ergonomic for your use case because when it comes time to actually invoke lower with a particular type-level argument, you need to supply the matching term-level argument explicitly:

lower @Zero SZero

or, since Haskell can infer the type-level argument automatically, just:

lower SZero

and then you have to ask yourself why not just use the term-level Zero directly, if you still need to pass a term-level SZero around to call lower.

Still, term-level parameters that take the form of either constraints or GADTs are really the only mechanism to have a type-level parameter affect the runtime behavior of a function in the way you want.