Danh sách độ dài và loại chữ cố định

Question

Tôi đang cố xác định loại cho danh sách độ dài cố định trong Haskell. Khi tôi sử dụng cách tiêu chuẩn để mã hóa các số tự nhiên thành các loại đơn nhất, mọi thứ đều hoạt động tốt. Tuy nhiên, khi tôi cố gắng xây dựng mọi thứ trên các loại chữ của GHC, tôi gặp phải rất nhiều vấn đề.

shot đầu tiên của tôi tại các loại danh sách mong muốn là

data List (n :: Nat) a where 
    Nil :: List 0 a 
    (:>) :: a -> List n a -> List (n+1) a 

mà tiếc là không cho phép viết một hàm zip với loại

zip :: List n a -> List n b -> List n (a,b) 

tôi có thể giải quyết vấn đề này bằng cách trừ đi 1 từ loại biến số n trong loại (:>):

data List (n :: Nat) a where 
    Nil :: List 0 a 
    (:>) :: a -> List (n-1) a -> List n a -- subtracted 1 from both n's 

Tiếp theo, tôi đã cố gắng để xác định một chức năng phụ thêm:

append :: List n1 a -> List n2 a -> List (n1 + n2) a 
append Nil  ys = ys 
append (x :> xs) ys = x :> (append xs ys) 

Thật không may, GHC nói với tôi

Couldn't match type ‘(n1 + n2) - 1’ with ‘(n1 - 1) + n2’ 

Thêm chế ((n1 + n2) - 1) ~ ((n1 - 1) + n2) để chữ ký không giải quyết được vấn đề kể từ GHC phàn nàn

Could not deduce ((((n1 - 1) - 1) + n2) ~ (((n1 + n2) - 1) - 1)) 
from the context (((n1 + n2) - 1) ~ ((n1 - 1) + n2)) 

Bây giờ, tôi rõ ràng bị bắt trong một số loại vòng lặp vô hạn.

Vì vậy, tôi muốn biết nếu nó có thể xác định một loại cho các danh sách có độ dài cố định sử dụng literals loại ở tất cả. Có lẽ tôi thậm chí có thể giám sát một thư viện cho chính xác mục đích này? Về cơ bản, yêu cầu duy nhất là tôi muốn viết một cái gì đó như List 3 a thay vì .

Answer 1

Đây không thực sự là câu trả lời.

Sử dụng https://hackage.haskell.org/package/ghc-typelits-natnormalise-0.2, đây

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE KindSignatures #-} 
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} 

import GHC.TypeLits 

data List (n :: Nat) a where 
    Nil :: List 0 a 
    (:>) :: a -> List n a -> List (n+1) a 

append :: List n1 a -> List n2 a -> List (n1 + n2) a 
append Nil  ys = ys 
append (x :> xs) ys = x :> (append xs ys) 

... biên dịch, vì vậy rõ ràng là nó đúng.

Answer 2

literals số Loại mực chưa có một cấu trúc mà chúng tôi có thể làm cảm ứng, và được xây dựng trong chế giải chỉ có thể tìm ra các trường hợp đơn giản nhất. Hiện tại, tốt hơn là nên gắn bó với Peano naturals.

Tuy nhiên, chúng ta vẫn có thể sử dụng các chữ như đường cú pháp.

{-# LANGUAGE 
    UndecidableInstances, 
    DataKinds, TypeOperators, TypeFamilies #-} 

import qualified GHC.TypeLits as Lit 

data Nat = Z | S Nat 

type family Lit n where 
    Lit 0 = Z 
    Lit n = S (Lit (n Lit.- 1)) 

Bây giờ bạn có thể viết List (Lit 3) a thay vì .