haskelltypestype-level-computation# 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
```

Solution

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.

- Using pattern synonyms to abstract implementation of text type
- How to avoid listing A as build dependency for internal library/executable E just because E depends on internal library L which depends on A?
- How is the Foldable instance of (,) useful?
- What is the proper way of wrapping an Int (not a general type) in another type if type safety is the only motive?
- What is the most practical way to express a dependency on a library for which we have a local git repository with some changes?
- Htmx POST to haskell servant handling optional field in FormUrlEncoded request
- Haskell fails to infer the return type of a monad after using the sequence operator
- Does extracting values from a multiple Value return in Haskell invoke the function more than once?
- How to specify c/c++ compiler on stack install command
- Why do I get "Unexpected reply type" from notify-send when using this Haskell notification server?
- Don't understand notation of morphisms in Monoid definition
- Foldln in haskell
- Is this property of a functor stronger than a monad?
- How to Instantiate a Custom Data Type with Record Syntax and Multiple Constructors
- How do I make a minimal working example for the a DBus server?
- Is it safe to downgrade Haskell stack version?
- Haskell, list of natural number
- unfamiliar syntax in Haskell / Clash function type signature
- foldM with monad State does not type check
- Why does my Runge-Kutta implementation oscillate to 0?
- How do I get the desired behavior in my TCP server?
- Why does the Haskell PVP describe new functions as non-breaking?
- How do I correctly use toLower in Haskell?
- How can I write a notification server in Haskell?
- Every Lens' is a Traversal'... how?
- How do I crate a value of type a{sv} for a call to org.freedesktop.Notifications.Notify via DBus?
- Web Scraping With Haskell
- Double exclamation marks in Haskell
- Haskell Servant POST FormUrlEncoded for (Vector String) field
- Confusion about list types in Haskell