Type for representing a list with 0 to 5 values

Question

I have an exercise where I have to define a type for representing a list with 0 to 5 values. First I thought I could solve this recursively like this:

data List a = Nil | Content a (List a) 

But I don't think this is the correct approach. Can you please give me a food of thought.

Answer 1

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.

Answer 2

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’