type pour représenter une liste avec 0 à 5 valeurs

J'ai un exercice où je dois définir un type pour représenter une liste avec 0 à 5 valeurs. J'ai d'abord pensé que je pouvais résoudre ce problème récursivement comme ceci:

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

Mais je ne pense pas que ce soit la bonne approche. Pouvez-vous, s'il vous plaît, me donner à réfléchir.

Je ne répondrai pas à votre exercice pour vous - pour les exercices, il vaut mieux trouver la réponse vous-même - mais voici un indice qui devrait vous conduire à la réponse: vous pouvez définir une liste avec 0 à 2 éléments comme

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

Maintenant, réfléchissez à comment étendre cela à cinq éléments.

Eh bien, une solution récursive est certainement la chose normale et en fait agréable dans Haskell, mais il est alors un peu difficile de limiter le nombre d'éléments. Donc, pour une solution simple au problème, considérons d'abord la solution stupide mais fonctionnelle donnée par bradm.

Avec la solution récursive, l'astuce consiste à passer une variable "compteur" le long de la récursivité, puis à désactiver la consistance de plus d'éléments lorsque vous atteignez le maximum autorisé. Cela peut se faire très bien avec 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)

alors

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

Par souci d'exhaustivité, permettez-moi d'ajouter une approche alternative "laide", qui est cependant plutôt basique.

Rappelons que Maybe ac'est un type dont les valeurs sont de la forme Nothingou Just xpour certains x :: a.

Par conséquent, en réinterprétant les valeurs ci-dessus, nous pouvons considérer Maybe acomme un "type de liste restreinte" où les listes peuvent avoir zéro ou un élément.

Maintenant, (a, Maybe a)ajoute simplement un élément de plus, c'est donc un "type de liste" où les listes peuvent avoir un ( (x1, Nothing)) ou deux ( (x1, Just x2)) éléments.

Par conséquent, Maybe (a, Maybe a)est un "type de liste" où les listes peuvent avoir zéro ( Nothing), un ( Just (x1, Nothing)) ou deux ( (Just (x1, Just x2)) éléments.

Vous devriez maintenant être en mesure de comprendre comment procéder. Permettez-moi de souligner à nouveau que ce n'est pas une solution pratique à utiliser, mais c'est (IMO) un bel exercice pour le comprendre de toute façon.

En utilisant certaines fonctionnalités avancées de Haskell, nous pouvons généraliser ce qui précède en utilisant une famille de types:

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