How can I generate term-level lists from a type-level ones?

Question

I'm trying to generate term-level values out of type-level ones. I have the following code

class Term a where
  type family Result a :: Type
  term :: Result a

instance (KnownSymbol s) => Term s where
  type instance Result s = String
  term = symbolVal (Proxy @s)

instance (KnownNat n) => Term n where
  type instance Result n = Integer
  term = natVal (Proxy @n)

This works just fine:

>>> :t term @"hello"
term @"hello" :: String
>>> term @"hello"
"hello"

How can I propagate this idea on type-level lists? When I try something like this

instance Term '[] where
  type instance Result ('[] :: [a]) = [a]
  term = []

instance (Term a, Term as) => Term (a ': as) where
  type instance Result (a ': as) = Result a ': Result as
  term = term @a : term @as

GHC says that RHS of Result (a ': as) has kind [*], but a type was expected.

• Expected a type, but ‘Result a : Result as’ has kind ‘[*]’
    • In the type ‘Result a : Result as’
      In the type instance declaration for ‘Result’
      In the instance declaration for ‘Term (a : as)’

I've got only one solution that compiles, but it expectedly evaluates only the first element:

instance (Term a, Term as) => Term (a ': as) where
  type instance Result (a ': as) = [Result a]
  term = [term @a]

>>> term @'["hello", "world"]
["hello"]

Is it possible to recursively transform type-level lists to terms?

Full code:

{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeFamilies        #-} 
{-# LANGUAGE TypeOperators       #-} 
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Term where

import           Data.Kind
import           Data.Proxy
import           GHC.TypeLits

class Term a where
  type family Result a :: Type
  term :: Result a

instance (KnownSymbol s) => Term s where
  type instance Result s = String
  term = symbolVal (Proxy @s)

instance (KnownNat n) => Term n where
  type instance Result n = Integer
  term = natVal (Proxy @n)

instance Term '[] where
  type instance Result ('[] :: [a]) = [a]
  term = []

instance (Term a, Term as) => Term (a ': as) where
  type instance Result (a ': as) = Result a ': Result as
  term = term @a : term @as

Answer 1

When GHC complains:

• Expected a type, but ‘Result a : Result as’ has kind ‘[*]’
• In the type ‘Result a : Result as’
  In the type instance declaration for ‘Result’
  In the instance declaration for ‘Term (a : as)’

The problem is that Result is supposed to give us the return type of term, so this ought to be the type of a term-level list (which will be of kind Type, or * in the older nomenclature¹). However we clearly have an expression for a type-level list (which is of kind [*] because Result a must be Type, which is the same as *).

In actual fact we want Result here to produce either [Integer] or [String] depending on whether the type-level list is of kind [Nat] or [Symbol]. We don't actually want to construct Result (a ': as) recursively depending on what as is. So lets change that to:

instance (Term a, Term as) => Term (a ': as) where
  type instance Result (a ': as) = [Result a]
  term = term @a : term @as

Now our error is:

• Couldn't match expected type ‘[Result a1]’
              with actual type ‘Result as’
• In the second argument of ‘(:)’, namely ‘term @as’
  In the expression: term @a : term @as
  In an equation for ‘term’: term = term @a : term @as

Aha. We haven't actually guaranteed to GHC's satisfaction that Result as will be a type of list on which Result a can be attached. As far as GHC knows those are two independent calls to a type family from two independent instances, there's no reason that one would always return a type that is a list of the other's result. But we know from the instances we actually want that this will in fact always hold, so maybe we can just add equality constraints?²

instance (Term a, Term as, Result as ~ [Result a]) => Term (a ': as) where
  type instance Result (a ': as) = [Result a]
  term = term @a : term @as

No compiler errors at all now! Lets try it:

>>> term @[1, 2, 3]

<interactive>:25:1: error:
    • Couldn't match type ‘Nat’ with ‘Integer’
        arising from a use of ‘term’
    • In the expression: term @[1, 2, 3]
      In an equation for ‘it’: it = term @[1, 2, 3]

Well, that's not exactly what we expected.

This one took me a while to figure out, but the problem is in the base instance for Term '[], not the recursive instance.

type instance Result ('[] :: [a]) = [a]

This says that term applied to an empty type level list is a term-level list containing the same type as in the type level list. It works when you directly use term @'[], because that type-level empty list is polykinded (just like empty lists at the term level are polymorphic). It can be a type level list of whatever kind we want. So if we take the resulting empty list at the term level and feed it into a context where a [Bool] is expected, GHC will dutifully infer that we must have been doing term @('[] :: [Bool]).

But when this empty list instance is used from the non-empty list instance, we aren't using a literal '[] which is free to be inferred as whatever kind we need. We use it when we get down to the end of a type level list of kind [Nat] or [Symbol]. That means we end up with something like Result ('[] :: [Nat]) = [Nat], i.e. the tail of our list is a term level list of Nat. Unfortunately we required that Result as ~ [Result a], and now that's not true; the last Result a is Integer and the last Result as is [Nat]. Even if GHC didn't pull us up, you can't cons an Integer onto a [Nat].

How to work around this is obscured because Term really has two parameters, not one. In Term a the kind of a also varies between instances. GHCI is aware of this and can tell us:

λ :info Term
type Term :: forall k. k -> Constraint
class Term a where
  type Result :: forall {k}. k -> *
  type family Result a
  term :: Result a

Note the type Term line; something like Monoid would show type Monoid :: * -> Constraint, or KnownNat would have type KnownNat :: Nat -> Constraint.

It's actually good, or we would have been shot down earlier. Because these two instance heads sure do look like they overlap³:

 instance (KnownSymbol s) => Term s 
 instance (KnownNat n) => Term n

But we're saved by the fact that they actually are distinct by instantiating the kind parameter k differently:

 instance (KnownSymbol s) => Term (s :: Symbol)
 instance (KnownNat n) => Term (n :: Nat)

If we make the kind parameter more explicit, we can make Result depend on the kind, rather than the type. Which is actually what we want anyway; type level 1, 2, and 3 all have a Result of Integer because they all have the kind Nat; we don't need to calculate a different resulting type for each individual Nat.

class Term (a :: k) where
  type family Result k :: Type
  term :: Result k

instance (KnownSymbol s) => Term (s :: Symbol) where
  type instance Result Symbol = String
  term = symbolVal (Proxy @s)

instance (KnownNat n) => Term (n :: Nat) where
  type instance Result Nat = Integer
  term = natVal (Proxy @n)

This also allows us to get rid of the annoying equality constraints in the recursive instance for lists, too. Result depends on the kind, and the compiler can see as well as we can that there is only one kind involved throughout the list (because a type-level list must have elements all of the same kind).

instance (Term a, Term as) => Term ((a ': as) :: [k]) where
  type instance Result [k] = [Result k]
  term = term @k @a : term @[k] @as

And now that we have the Result depending on the kind and not the type, we can do this for the base case:

instance Term ('[] :: [k]) where
  type instance Result [k] = [Result k]
  term = []

To be honest I'm not 100% certain why this works. We depend for Result [k] on there being another Term instance that supplies Result k, but we don't have a constraint guaranteeing that such an instance will exist (and I don't know how we would write one, without a type with kind k actually available to pass to Term). But it does work:

>>> term @_ @3
3
it :: Integer

>>> term @_ @[1, 2, 3]
[1,2,3]
it :: [Integer]

>>> term @_ @["hello", "world"]
["hello","world"]
it :: [String]

The big downside though is now there's an extra parameter we have to explicitly pass to term. GHC can infer what it is (which is why we could use @_), but it has to come first because it is the kind of a following parameter.

The simplest way I came up with to fix that was to rename term to term', and provide a new term that marks the kind parameter as inferred so that it need not (and cannot) be specified with a type application. This needs GHC 9 or later though.

term :: forall {k} (a :: k). Term (a :: k) => Result k
term = term' @k @a

But then I thought of a better way. It was already irking me slightly that we have to repeat the identical definition of type instance Result [k] = [Result k] in both of the instances pertaining to lists. That's because the instance depends on the actual type, but the type family Result depends only on its kind, so where we have two instances covering different types of the same kind we end up needing redundant definitions. To me that was already a sign that this isn't really an associated type family of the class, but would be better as a stand-alone type family.

type family Demote k where
  Demote Symbol = String
  Demote Nat = Integer
  Demote [k] = [Demote k]

Having taken the type family out of the class, it would be great if we didn't need the explicit kind parameter k any more (it'll still be there as an implicit parameter, but it won't clutter up our type applications). Unfortunately to call Demote we still need an explicit reference to the kind. We don't have that if our class definition is class Term a rather than class Term (a :: k). But if we add another layer of indirection, we can make a type synonym (doesn't even have to be a type family!) that gets the kind of a type⁴:

type KindOf (a :: k) = k

class Term a where
  term :: Demote (KindOf a)

Now it finally all works!

>>> term @19
19
it :: Integer

>>> term @[10, 5, 0]
[10,5,0]
it :: [Integer]

>>> term @["take", "that", "typechecker"]
["take","that","typechecker"]
it :: [String]

The only (minor?) problem is that now term @'[] no longer works on its own, because it needs to actually know what the kind of the empty list is (to resolve the Demote type family) instead of giving us a polymorphic empty list.

>>> term @'[]

<interactive>:26:1: error:
    • Couldn't match type: Result k0
                     with: Result k
      Expected: [Result k]
        Actual: [Result k0]
      NB: ‘Result’ is a non-injective type family
      The type variable ‘k0’ is ambiguous
    • In the ambiguity check for the inferred type for ‘it’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      When checking the inferred type
        it :: forall {k}. [Result k]

>>> term @('[] :: [Symbol])
[]
it :: [String]

Here is the final working module I ended up with:

{-# LANGUAGE AllowAmbiguousTypes, DataKinds, PolyKinds, FlexibleInstances, ScopedTypeVariables, TypeApplications, TypeFamilies, TypeOperators #-}

module Term
where

import GHC.Types
import GHC.TypeLits

import Data.Proxy

type KindOf (a :: k) = k

type family Demote k where
  Demote Symbol = String
  Demote Nat = Integer
  Demote [k] = [Demote k]


class Term a where
  term :: Demote (KindOf a)

instance (KnownSymbol s) => Term (s :: Symbol) where
  term = symbolVal (Proxy @s)

instance (KnownNat n) => Term (n :: Nat) where
  term = natVal (Proxy @n)

instance Term ('[] :: [k]) where
  term = []

instance (Term a, Term as) => Term ((a ': as) :: [k]) where
  term = term @a : term @as

---

¹ I think GHC says "expected a type" to mean it expected Type/* here because that's less confusing to beginners than something like "Kind mismatch, expected *, actual [*]".

---

² This is a common trick to add extra "axioms" to GHC's type inference in instances. If the constraints on an instance include foo ~ bar, then GHC will assume that is true in general when type-checking the instance, and will check that it's actually true (for the particular types involved) when using the instance. If it's something you "know" will always be true but can't prove in Haskell, then that check will always pass; this allows you to make use of a truth that you cannot actually prove in Haskell.

---

³ Remembering that which instances applies in a given situation must be able to be determined without considering their constraints!

---

⁴ I had a hunch that I was rediscovering a wheel here, and sure enough that exact definition for KindOf already exists in the singletons package. singletons contains a lot of advanced machinery for doing this sort of type-level-corresponding-to-term-level stuff; I don't know off-hand exactly what to point you at, but you could in fact replace all of your Term class with something from singletons and it'll already work and be more general. However singletons is quite an advanced package, so not the easiest thing to learn.

If you plan on using this sort of code for ongoing practical purposes, I would highly recommend you invest the effort to learn how to use singletons. It may be better than writing it yourself.

If you're writing this to learn how these kinds of type level programming concepts work, then singletons will have lots of examples of just how far you can push this, but its implementation may be hard to comprehend for a relative novice.