Làm thế nào để `HFix` hoạt động trong gói multirec của Haskell?

Question

Tôi hiểu bộ tổ hợp loại điểm cố định thường xuyên và tôi nghĩ rằng tôi hiểu các bộ tổ hợp loại cố định loại n cao hơn, nhưng HFix là eludes tôi. Bạn có thể đưa ra một ví dụ về một tập hợp các kiểu dữ liệu và các điểm cố định (có nguồn gốc thủ công) mà bạn có thể áp dụng HFix cho.

Answer 1

Tham chiếu tự nhiên là giấy Generic programming with fixed points for mutually recursive datatypes nơi giải thích multirec package.

HFix là bộ kết hợp loại điểm cố định cho các loại dữ liệu đệ quy lẫn nhau. Nó được giải thích trong Phần 3.2 trên báo, nhưng ý tưởng là để khái quát mô hình này:

Fix :: (∗ -> ∗) -> ∗ 
Fix2 :: (∗ -> ∗ -> ∗) -> (∗ -> ∗ -> ∗) -> ∗ 

để

Fixn :: ((∗ ->)^n * ->)^n ∗ 
≈ 
Fixn :: (*^n -> *)^n -> * 

Để hạn chế bao nhiêu loại nó một điểm cố định trên, họ sử dụng các hàm tạo kiểu thay vì *^n. Chúng đưa ra một ví dụ về kiểu dữ liệu AST, đệ quy đệ quy trên ba loại trong bài báo. Tôi cung cấp cho bạn có lẽ ví dụ đơn giản nhất thay thế. Hãy chúng tôi HFix kiểu dữ liệu này:

data Even = Zero | ESucc Odd deriving (Show,Eq) 
data Odd = OSucc Even  deriving (Show,Eq) 

Chúng ta hãy giới thiệu GADT cụ gia đình cho datatype này như được thực hiện trong phần 4,1

data EO :: * -> * where 
    E :: EO Even 
    O :: EO Odd 

EO Even sẽ có nghĩa là chúng tôi đang triển khai xung quanh một số chẵn. Chúng tôi cần các phiên bản El để làm việc này, cho biết nhà xây dựng cụ thể chúng tôi đang đề cập đến khi viết EO Even và EO Odd tương ứng.

instance El EO Even where proof = E 
instance El EO Odd where proof = O 

Chúng được sử dụng như những hạn chế đối với HFunctor instance cho I.

Bây giờ chúng ta hãy định nghĩa mẫu functor cho kiểu dữ liệu chẵn và lẻ. Chúng tôi sử dụng bộ kết hợp từ thư viện.Các :>: loại thẻ constructor một giá trị với chỉ số loại của nó:

type PFEO = U  :>: Even -- ≈ Zero ::()  -> EO Even 
     :+: I Odd :>: Even -- ≈ ESucc :: EO Odd -> EO Even 
     :+: I Even :>: Odd -- ≈ OSucc :: EO Even -> EO Odd 

Bây giờ chúng ta có thể sử dụng HFix để tổ chức đám cưới xung quanh mô hình này functor:

type Even' = HFix PFEO Even 
type Odd' = HFix PFEO Odd 

Những hiện nay có đẳng cấu với EO Thậm chí và EO Odd, và chúng tôi có thể sử dụng hfrom and hto functions nếu chúng ta làm cho nó một thể hiện của Fam:

type instance PF EO = PFEO 

instance Fam EO where 
    from E Zero  = L (Tag U) 
    from E (ESucc o) = R (L (Tag (I (I0 o)))) 
    from O (OSucc e) = R (R (Tag (I (I0 e)))) 
    to E (L (Tag U))   = Zero 
    to E (R (L (Tag (I (I0 o))))) = ESucc o 
    to O (R (R (Tag (I (I0 e))))) = OSucc e 

Một chút thử nghiệm đơn giản:

test :: Even' 
test = hfrom E (ESucc (OSucc Zero)) 

test' :: Even 
test' = hto E test 

*HFix> test' 
ESucc (OSucc Zero) 

Một thử nghiệm ngớ ngẩn với một Đại số biến Even và Odd s giá trị Int của họ:

newtype Const a b = Const { unConst :: a } 

valueAlg :: Algebra EO (Const Int) 
valueAlg _ = tag (\U    -> Const 0) 
      & tag (\(I (Const x)) -> Const (succ x)) 
      & tag (\(I (Const x)) -> Const (succ x)) 

value :: Even -> Int 
value = unConst . fold valueAlg E