Type for representing a list with 0 to 5 values

Well, a recursive solution is certainly the normal and in fact nice thing in Haskell, but it's a bit tricky to limit the number of elements then. So, for a simple solution to the problem, first consider the stupid-but-working one given by bradm.

With the recursive solution, the trick is to pass a “counter” variable down the recursion, and then disable consing more elements when you reach the max allowed. This can be done nicely with a GADT:

{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeInType, StandaloneDeriving #-}

import Data.Kind
import GHC.TypeLits

infixr 5 :#
data ListMax :: Nat -> Type -> Type where
  Nil :: ListMax n a
  (:#) :: a -> ListMax n a -> ListMax (n+1) a

deriving instance (Show a) => Show (ListMax n a)

Then

*Main> 0:#1:#2:#Nil :: ListMax 5 Int
0 :# (1 :# (2 :# Nil))

*Main> 0:#1:#2:#3:#4:#5:#6:#Nil :: ListMax 5 Int

<interactive>:13:16: error:
    • Couldn't match type ‘1’ with ‘0’
      Expected type: ListMax 0 Int
        Actual type: ListMax (0 + 1) Int
    • In the second argument of ‘(:#)’, namely ‘5 :# 6 :# Nil’
      In the second argument of ‘(:#)’, namely ‘4 :# 5 :# 6 :# Nil’
      In the second argument of ‘(:#)’, namely ‘3 :# 4 :# 5 :# 6 :# Nil’

For the sake of completeness, let me add an "ugly" alternative approach, which is however rather basic.

Recall that Maybe a is a type whose values are of the form Nothing or Just x for some x :: a.

Hence, by reinterpreting the values above, we can regard Maybe a as a "restricted list type" where lists can have either zero or one element.

Now, (a, Maybe a) simply adds one more element, so it is a "list type" where lists can have one ((x1, Nothing)) or two ((x1, Just x2)) elements.

Therefore, Maybe (a, Maybe a) is a "list type" where lists can have zero (Nothing), one (Just (x1, Nothing)), or two ((Just (x1, Just x2)) elements.

You should now be able to understand how to proceed. Let me stress again that this is not a convenient solution to use, but it is (IMO) a nice exercise to understand it anyway.

---

Using some advanced features of Haskell, we can generalize the above using a type family:

type family List (n :: Nat) (a :: Type) :: Type where
    List 0 a = ()
    List n a = Maybe (a, List (n-1) a)

I won’t answer your exercise for you — for exercises, it’s better to figure out the answer yourself — but here’s a hint which should lead you to the answer: you can define a list with 0 to 2 elements as

data List a = None | One a | Two a a

Now, think about how can you extend this to five elements.