Lower type level values to term level in Haskell

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


  • 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.