wpisz nazwę reprezentującą listę o wartości od 0 do 5

Mam ćwiczenie, w którym muszę zdefiniować typ reprezentujący listę z wartościami od 0 do 5. Najpierw pomyślałem, że mogę rozwiązać to tak rekurencyjnie:

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

Ale nie sądzę, że jest to właściwe podejście. Czy możesz mi dać do myślenia.

Nie odpowiem za twoje ćwiczenie dla ciebie - w przypadku ćwiczeń lepiej jest samemu znaleźć odpowiedź - ale oto wskazówka, która powinna doprowadzić cię do odpowiedzi: możesz zdefiniować listę zawierającą od 0 do 2 elementów jako

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

Zastanów się teraz, jak możesz rozszerzyć to na pięć elementów.

Cóż, rekurencyjne rozwiązanie jest z pewnością normalną i faktycznie fajną rzeczą w Haskell, ale wtedy nieco trudniej jest ograniczyć liczbę elementów. Tak więc, aby uzyskać proste rozwiązanie problemu, najpierw rozważ głupią, ale działającą, podaną przez bradm.

W przypadku rozwiązania rekurencyjnego sztuczką jest przekazywanie zmiennej „counter” w dół rekurencji, a następnie wyłączenie zużywania większej liczby elementów po osiągnięciu maksymalnej dozwolonej. Można to zrobić ładnie za pomocą 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)

Następnie

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

Dla kompletności dodam „brzydkie” podejście alternatywne, które jednak jest raczej podstawowe.

Przypomnijmy, że Maybe ajest to typ, którego wartości mają formę Nothinglub Just xdla niektórych x :: a.

Dlatego, interpretując powyższe wartości, możemy uznać Maybe aza „ograniczony typ listy”, w którym listy mogą zawierać zero lub jeden element.

Teraz (a, Maybe a)po prostu dodaje jeszcze jeden element, więc jest to „typ listy”, w którym listy mogą zawierać jeden ( (x1, Nothing)) lub dwa ( (x1, Just x2)) elementy.

Dlatego Maybe (a, Maybe a)jest to „typ listy”, w którym listy mogą zawierać zero ( Nothing), jeden ( Just (x1, Nothing)) lub dwa ( (Just (x1, Just x2)) elementy.

Powinieneś teraz być w stanie zrozumieć, jak postępować. Chciałbym jeszcze raz podkreślić, że nie jest to wygodne rozwiązanie, ale jest to (IMO) przyjemne ćwiczenie, aby je zrozumieć.

Korzystając z niektórych zaawansowanych funkcji Haskell, możemy uogólnić powyższe za pomocą rodziny typów:

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