Làm thế nào để mổ xẻ một SNAT (độc thân)

Question

Tôi đang thử nghiệm với các loại depedent trong Haskell và đi qua sau trong paper của 'độc thân' gói:

replicate2 :: forall n a. SingI n => a -> Vec a n 
replicate2 a = case (sing :: Sing n) of 
    SZero -> VNil 
    SSucc _ -> VCons a (replicate2 a) 

Vì vậy, tôi đã cố gắng để thực hiện điều này bản thân mình, chỉ cần toget một cảm giác như thế nào nó hoạt động:

{-# LANGUAGE DataKinds   #-} 
{-# LANGUAGE GADTs    #-} 
{-# LANGUAGE KindSignatures  #-} 
{-# LANGUAGE TypeOperators  #-} 
{-# LANGUAGE RankNTypes   #-} 
{-# LANGUAGE ScopedTypeVariables #-} 

import   Data.Singletons 
import   Data.Singletons.Prelude 
import   Data.Singletons.TypeLits 

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

infixr 5 :> 

replicateV :: SingI n => a -> V n a 
replicateV = replicateV' sing 
    where replicateV' :: Sing n -> a -> V n a 
     replicateV' sn a = case sn of 
      SNat -> undefined -- what can I do with this? 

Bây giờ vấn đề là các Sing dụ cho Nat không có SZero hoặc SSucc. Chỉ có một hàm tạo được gọi là SNat.

> :info Sing 
data instance Sing n where 
    SNat :: KnownNat n => Sing n 

này khác với độc thân khác mà cho phép kết hợp, chẳng hạn như STrue và SFalse, chẳng hạn như trong những điều sau đây (vô dụng) ví dụ:

data Foo :: Bool -> * -> * where 
    T :: a -> Foo True a 
    F :: a -> Foo False a 

foo :: forall a b. SingI b => a -> Foo b a 
foo a = case (sing :: Sing b) of 
    STrue -> T a 
    SFalse -> F a 

Bạn có thể sử dụng fromSing để có được một loại cơ sở, nhưng điều này tất nhiên không cho phép GHC kiểm tra loại vector đầu ra:

-- does not typecheck 
replicateV2 :: SingI n => a -> V n a 
replicateV2 = replicateV' sing 
    where replicateV' :: Sing n -> a -> V n a 
     replicateV' sn a = case fromSing sn of 
       0 -> Nil 
       n -> a :> replicateV2 a 

Vì vậy, câu hỏi của tôi: cách triển khai replicateV?

EDIT

Câu trả lời được đưa ra bởi erisco giải thích lý do tại sao cách tiếp cận của tôi về giải cấu trúc một SNat không hoạt động. Nhưng ngay cả với thư viện type-natural, tôi không thể triển khai replicateV cho loại dữ liệu Vbằng cách sử dụng GHC tích hợp Nat loại.

Ví dụ đoạn mã sau biên dịch:

replicateV :: SingI n => a -> V n a 
replicateV = replicateV' sing 
    where replicateV' :: Sing n -> a -> V n a 
     replicateV' sn a = case TN.sToPeano sn of 
      TN.SZ  -> undefined 
      (TN.SS sn') -> undefined 

Nhưng điều này dường như không cung cấp đủ thông tin để trình biên dịch để suy ra dù n là 0 hay không. Ví dụ sau đây đưa ra một lỗi biên dịch:

replicateV :: SingI n => a -> V n a 
replicateV = replicateV' sing 
    where replicateV' :: Sing n -> a -> V n a 
     replicateV' sn a = case TN.sToPeano sn of 
      TN.SZ  -> Nil 
      (TN.SS sn') -> undefined 

này cung cấp cho các lỗi sau:

src/Vec.hs:25:28: error: 
    • Could not deduce: n1 ~ 0 
     from the context: TN.ToPeano n1 ~ 'TN.Z 
     bound by a pattern with constructor: 
        TN.SZ :: forall (z0 :: TN.Nat). z0 ~ 'TN.Z => Sing z0, 
       in a case alternative 
     at src/Vec.hs:25:13-17 
     ‘n1’ is a rigid type variable bound by 
     the type signature for: 
      replicateV' :: forall (n1 :: Nat) a1. Sing n1 -> a1 -> V n1 a1 
     at src/Vec.hs:23:24 
     Expected type: V n1 a1 
     Actual type: V 0 a1 
    • In the expression: Nil 
     In a case alternative: TN.SZ -> Nil 
     In the expression: 
     case TN.sToPeano sn of { 
      TN.SZ -> Nil 
      (TN.SS sn') -> undefined } 
    • Relevant bindings include 
     sn :: Sing n1 (bound at src/Vec.hs:24:21) 
     replicateV' :: Sing n1 -> a1 -> V n1 a1 (bound at src/Vec.hs:24:9) 

Vì vậy, vấn đề ban đầu của tôi vẫn còn, tôi vẫn không thể làm bất cứ điều gì hữu ích với SNat.

Answer 1

Từ nhận xét, tôi lo lắng rằng tôi phải thiếu điều gì đó tuyệt vời rõ ràng, nhưng đây là việc tôi thực hiện nó.Toàn bộ các điểm:

replicate2 :: forall n a. SingI n => a -> Vec a n 
replicate2 a = case (sing :: Sing n) of 
    SZero -> VNil 
    SSucc _ -> VCons a (replicate2 a) 

là, để trở VNil :: Vec a 0 khi hàm có chung lợi nhuận loại Vec a n, bạn cần phải chuyên các n-0, và mô hình khớp trên GADTs cung cấp một cách để làm điều này , miễn là bạn có một hàm tạo, như là SZero, ngụ ý n ~ 0.

Hiện tại, SNat s trong gói singleton không có hàm tạo nào như vậy. Cách duy nhất để có được một, như xa như tôi có thể thấy, là xây dựng một loại singleton hoàn toàn mới cho naturals và thực hiện các loại gia đình cần thiết. Có lẽ bạn có thể làm điều đó theo cách kết thúc tốt đẹp Nat s, vì vậy bạn gần với SZero :: Sing (SN 0), SNonZero :: Sing (SN n) hơn là xây dựng Peano, nhưng tôi không biết.

Tất nhiên, có một cách khác để chuyên chức năng trả về Vec a n để trả về Vec a 0, cụ thể là các lớp loại.

Nếu bạn sẵn sàng từ bỏ một số máy móc đơn lẻ rõ ràng và chuyển sang loại lớp học (và cũng cho phép chồng chéo và không thể xác định được trường hợp), những điều sau đây có vẻ hoạt động. Tôi đã phải sửa đổi một chút định nghĩa của V để sử dụng n :- 1 thay vì n :+ 1, nhưng tôi không nghĩ rằng gây ra sự cố.

{-# LANGUAGE DataKinds    #-} 
{-# LANGUAGE GADTs     #-} 
{-# LANGUAGE KindSignatures  #-} 
{-# LANGUAGE TypeOperators   #-} 
{-# LANGUAGE RankNTypes   #-} 
{-# LANGUAGE ScopedTypeVariables #-} 

{-# LANGUAGE MultiParamTypeClasses #-} 
{-# LANGUAGE FlexibleInstances  #-} 
{-# LANGUAGE FlexibleContexts  #-} 
{-# LANGUAGE OverlappingInstances #-} 
{-# LANGUAGE UndecidableInstances #-} 

import   Data.Singletons 
import   Data.Singletons.Prelude 
import   Data.Singletons.TypeLits 

data V :: Nat -> * -> * where 
    Nil :: V 0 a 
    (:>) :: a -> V (n :- 1) a -> V n a 

infixr 5 :> 

class VC n a where 
    replicateV :: a -> V n a 

instance VC 0 a where 
    replicateV _ = Nil 

instance VC (n :- 1) a => VC n a where 
    replicateV x = x :> replicateV x 

instance (Show a) => Show (V n a) where 
    show Nil = "Nil" 
    show (x :> v) = show x ++ " :> " ++ show v 

headV :: V (n :+ 1) a -> a 
headV (x :> _) = x 

tailV :: ((n :+ 1) :- 1) ~ n => V (n :+ 1) a -> V n a 
tailV (_ :> v) = v 

main = do print (replicateV False :: V 0 Bool) 
      print (replicateV 1  :: V 1 Int) 
      print (replicateV "Three" :: V 3 String) 

Answer 2

Có hai khái niệm về naturals khi chơi ở đây. Một là "naturals chữ" (tức là 0, 1, 2, v.v.) và cái còn lại là "Peano naturals" (tức là Z, S Z, S (S Z), v.v.). Một trong những giấy được sử dụng rõ ràng là Peano naturals nhưng một trong những singletons sử dụng là naturals chữ.

Rất may, có một gói khác được gọi là type-natural xác định số tự nhiên Peano cũng như conversion to literal naturals và conversion from literal naturals.