тип для представления списка от 0 до 5 значений

У меня есть упражнение, в котором я должен определить тип для представления списка с 0 до 5 значений. Сначала я подумал, что могу решить это рекурсивно так:

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

Но я не думаю, что это правильный подход. Можете ли вы дать мне пищу мысли.

Я не буду отвечать за ваше упражнение - для упражнений лучше выяснить ответ самостоятельно - но вот подсказка, которая должна привести вас к ответу: вы можете определить список с 0 до 2 элементов как

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

Теперь подумайте, как вы можете расширить это до пяти элементов.

Что ж, рекурсивное решение - это, конечно, нормальная и на самом деле приятная вещь в Haskell, но тогда немного сложно ограничить количество элементов. Итак, для простого решения проблемы, сначала рассмотрим глупый, но работающий, заданный bradm.

При использовании рекурсивного решения задача состоит в том, чтобы передать переменную «counter» по рекурсии, а затем отключить использование большего количества элементов, когда вы достигнете максимально допустимого значения. Это можно сделать красиво с помощью 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)

затем

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

Для полноты позвольте мне добавить «некрасивый» альтернативный подход, который, однако, довольно прост.

Напомним, что Maybe aэто тип, значения которого имеют форму Nothingили Just xдля некоторых x :: a.

Следовательно, переосмысливая приведенные выше значения, мы можем рассматривать их Maybe aкак «ограниченный тип списка», где списки могут иметь либо ноль, либо один элемент.

Теперь (a, Maybe a)просто добавьте еще один элемент, так что это «тип списка», в котором списки могут иметь один ( (x1, Nothing)) или два ( (x1, Just x2)) элемента.

Следовательно, Maybe (a, Maybe a)это «тип списка», в котором списки могут иметь элементы zero ( Nothing), one ( Just (x1, Nothing)) или two ( (Just (x1, Just x2)).

Теперь вы должны понимать, как действовать дальше. Позвольте мне еще раз подчеркнуть, что это не удобное решение для использования, но это (IMO) хорошее упражнение, чтобы понять его в любом случае.

Используя некоторые расширенные возможности Haskell, мы можем обобщить вышесказанное, используя семейство типов:

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