ketik untuk mewakili daftar dengan nilai 0 hingga 5

14

Saya memiliki latihan di mana saya harus mendefinisikan tipe untuk mewakili daftar dengan nilai 0 hingga 5. Pertama saya pikir saya bisa menyelesaikan ini secara rekursif seperti ini:

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

Tapi saya rasa ini bukan pendekatan yang tepat. Bisakah Anda memberi saya makanan pemikiran.

haskell mayerph
sumber

Jawaban:

12

Saya tidak akan menjawab latihan Anda untuk Anda - untuk latihan, lebih baik untuk mengetahui jawabannya sendiri - tetapi inilah petunjuk yang akan mengarahkan Anda ke jawabannya: Anda dapat mendefinisikan daftar dengan 0 hingga 2 elemen sebagai

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

Sekarang, pikirkan bagaimana Anda bisa memperpanjang ini hingga lima elemen.

bradrn
sumber
10

Nah, solusi rekursif tentu merupakan hal yang normal dan bahkan menyenangkan di Haskell, tetapi agak sulit untuk membatasi jumlah elemen saat itu. Jadi, untuk solusi sederhana untuk masalah ini, pertama-tama pertimbangkan yang bodoh tapi berfungsi yang diberikan oleh bradm.

Dengan solusi rekursif, triknya adalah untuk melewatkan variabel "penghitung" ke rekursi, dan kemudian menonaktifkan elemen lainnya ketika Anda mencapai jumlah maksimum yang diizinkan. Ini dapat dilakukan dengan baik dengan 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)

Kemudian

*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’
leftaroundabout
sumber
Terima kasih banyak. Karena ini latihan pemula, saya pikir itu pendekatan yang lebih mudah. Tapi saya akan memikirkan pendekatan Anda juga.
mayerph
7

Demi kelengkapan, izinkan saya menambahkan pendekatan alternatif "jelek", yang bagaimanapun agak mendasar.

Ingat itu Maybe aadalah tipe yang nilainya dari bentuk Nothingatau Just xuntuk beberapa x :: a.

Oleh karena itu, dengan menafsirkan kembali nilai-nilai di atas, kita dapat menganggapnya Maybe asebagai "tipe daftar terbatas" di mana daftar dapat memiliki nol atau satu elemen.

Sekarang, (a, Maybe a)cukup tambahkan satu elemen lagi, jadi itu adalah "tipe daftar" di mana daftar dapat memiliki satu ( (x1, Nothing)) atau dua ( (x1, Just x2)) elemen.

Oleh karena itu, Maybe (a, Maybe a)adalah "tipe daftar" di mana daftar dapat memiliki elemen nol ( Nothing), satu ( Just (x1, Nothing)), atau dua ( (Just (x1, Just x2)).

Anda sekarang harus dapat memahami bagaimana melanjutkan. Biarkan saya tekankan lagi bahwa ini bukan solusi yang mudah digunakan, tetapi (IMO) latihan yang bagus untuk memahaminya.

Menggunakan beberapa fitur canggih dari Haskell, kita dapat menggeneralisasi di atas menggunakan tipe keluarga:

type family List (n :: Nat) (a :: Type) :: Type where
    List 0 a = ()
    List n a = Maybe (a, List (n-1) a)
chi
sumber
Jawaban ini dapat diperluas dengan jenis keluarga dari daftar max-length n berdasarkan mungkin .
leftaroundabout
@leftaroundabout Done. Itu mungkin terlalu banyak untuk pemula, tetapi saya tetap menambahkannya.
chi
paling banyak tiga as di Either () (a, Either () (a, Either () (a, Either () ())))... aljabar tipe menarik foldr (.) id (replicate 3 $ ([0] ++) . liftA2 (+) [1]) $ [0] == [0,1,2,3],.
Will Ness