tipo para representar una lista con 0 a 5 valores

Bueno, una solución recursiva es ciertamente lo normal y de hecho agradable en Haskell, pero es un poco complicado limitar el número de elementos en ese momento. Entonces, para una solución simple al problema, primero considere la estúpida pero funcional dada por bradm.

Con la solución recursiva, el truco consiste en pasar una variable de "contador" por la recursividad y luego deshabilitar el consumo de más elementos cuando se alcanza el máximo permitido. Esto se puede hacer muy bien con un 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)

Entonces

*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’

En aras de la exhaustividad, permítanme agregar un enfoque alternativo "feo", que sin embargo es bastante básico.

Recuerde que Maybe a es un tipo cuyos valores tienen la forma Nothing o Just x para algunos x :: a.

Por lo tanto, al reinterpretar los valores anteriores, podemos considerar Maybe a como un "tipo de lista restringida" donde las listas pueden tener cero o un elemento.

Ahora, (a, Maybe a) simplemente agrega un elemento más, por lo que es un "tipo de lista" donde las listas pueden tener uno ((x1, Nothing)) o dos ((x1, Just x2)) elementos.

Por lo tanto, Maybe (a, Maybe a) es un "tipo de lista" donde las listas pueden tener cero (Nothing), uno (Just (x1, Nothing)) o dos ((Just (x1, Just x2)) elementos.

Ahora debería poder entender cómo proceder. Permítanme enfatizar nuevamente que esta no es una solución conveniente de usar, pero es (IMO) un buen ejercicio para entenderlo de todos modos.

Usando algunas características avanzadas de Haskell, podemos generalizar lo anterior usando una familia de tipos:

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