劈裂GHC

Question

類型級列表

我有困難的時候，說服GHC該列表操作的某些屬性 是真實的。之前我提供了我 工作的代碼，我給我感興趣的屬性的一個簡單的例子 假設我們有一些類型級列表xs：

xs ~ '[ 'A, 'B, 'C, 'D, 'E, 'F ] 

我們降一些元素，並採取 元素的同一個號碼：

Drop 2 xs ~ '[ 'C, 'D, 'E, 'F ] 
TakeReverse 2 xs ~ '[ 'B, 'A ] 

這應該是顯而易見的是，如果我使用的2後繼申請Drop和TakeReverse ，然後我就可以爆開的的 Drop 2 xs，並把它的頂部TakeReverse 2 xs：

Drop 3 xs ~ '[ 'D, 'E, 'F ] 
TakeReverse 3 xs ~ '[ 'C, 'B, 'A ] 

下面的代碼中有一個名爲moveRight函數試圖 使用這個屬性。我已經將我的實際代碼縮減爲一個有點小的例子， 說明了這個問題並且沒有依賴關係。

{-# LANGUAGE DataKinds   #-} 
{-# LANGUAGE FlexibleContexts  #-} 
{-# LANGUAGE OverloadedStrings #-} 
{-# LANGUAGE PolyKinds   #-} 
{-# LANGUAGE ScopedTypeVariables #-} 
{-# LANGUAGE TypeFamilies   #-} 
{-# LANGUAGE TypeOperators  #-} 
{-# LANGUAGE GADTs    #-} 
{-# LANGUAGE UndecidableInstances #-} 
module Minimal where 

import Data.Type.Equality 

data Nat = Z | S Nat 

data Natty (n :: Nat) where 
    Zy :: Natty 'Z 
    Sy :: Natty n -> Natty ('S n) 

data HRec (vs :: [*]) where 
    HRecNil :: HRec '[] 
    HRecCons :: x -> HRec xs -> HRec (x ': xs) 

data HProxy (vs :: [k]) where 
    HProxyNil :: HProxy '[] 
    HProxyCons :: HProxy xs -> HProxy (x ': xs) 

data Parts n rs = Parts 
    { partLeft :: HRec (Drop n rs) 
    , partRight :: HRec (TakeReverse n rs) 
    , partNatty :: Natty n 
    , partProxy :: HProxy rs 
    } 

-- The type families Drop, Take, and TakeReverse 
-- are all partial. 
type family Drop (n :: Nat) (xs :: [k]) :: [k] where 
    Drop 'Z xs = xs 
    Drop ('S n) (x ': xs) = Drop n xs 

type family Take (n :: Nat) (xs :: [k]) :: [k] where 
    Take 'Z xs = '[] 
    Take ('S n) (x ': xs) = x ': Take n xs 

type family TakeReverse (n :: Nat) (xs :: [k]) :: [k] where 
    TakeReverse n xs = TakeReverseHelper '[] n xs 

type family TakeReverseHelper (ys :: [k]) (n :: Nat) (xs :: [k]) :: [k] where 
    TakeReverseHelper res 'Z xs = res 
    TakeReverseHelper res ('S n) (x ': xs) = TakeReverseHelper (x ': res) n xs 

moveRight :: Parts n rs -> Parts (S n) rs 
moveRight (Parts pleft@(HRecCons pleftHead _) pright natty proxy) = 
    case dropOneProof natty proxy of 
    Refl -> Parts (dropOne pleft) (HRecCons pleftHead pright) (Sy natty) proxy 

dropOneProof :: Natty n -> HProxy rs -> (Drop ('S n) rs :~: Drop ('S 'Z) (Drop n rs)) 
dropOneProof Zy _ = Refl 
dropOneProof (Sy n) (HProxyCons rs) = case dropOneProof n rs of 
    Refl -> Refl 

dropOne :: HRec rs -> HRec (Drop ('S 'Z) rs) 
dropOne (HRecCons _ rs) = rs 

此代碼不會因爲moveRight編譯。基本上，我能 證明，從左邊下降一個額外的元素給它 正確的類型，但我不能表明，添加這個元素向右 側使其具有正確的類型。

我真的很樂意接受任何改變。我可以改變類型系列， 引入額外的證人等，只要moveRight變成 可能寫。

如果我需要進一步澄清什麼，我試圖做的，請讓我知道。謝謝。

Answer 1

你表示的問題是，你儘量使分割的位置明確的，但不執行位置指數的有效性。

因爲它是目前moveRight :: Parts n rs -> Parts (S n) rs無法執行，因爲如果n是出界，Take和其他類型的家庭應用不能減少，因此沒有值可以在結果中給出。

有很多方法可以解決這個問題。最簡單的就是使類型的背景下明確的左右兩部分：

type HZipper xs ys = (HRec xs, HRec ys) 

moveRight :: HZipper xs (y ': ys) -> HZipper (y ': xs) ys 
moveRight'(xs, HCons y ys) = (HCons y xs, ys) 

這實際上是同樣強勁representatation你原來Parts。只要我們在那裏執行n索引的邊界。這是因爲這兩種類型都表示整個列表和分割的確切位置。從HZipper xs ys，原始類型列表可以被計算爲Reverse xs ++ ys與適當的++和Reverse型家庭。這有時候不太方便，但在優化方面HZipper有更簡單的內部。

另外，也可以存在上隱藏分割的位置。在任何情況下，這需要證明寫moveRight：

import Data.Type.Equality 
import Data.Proxy 

data HRec vs where 
    HNil :: HRec '[] 
    HCons :: x -> HRec xs -> HRec (x ': xs) 

type family (++) xs ys where 
    '[] ++ ys = ys 
    (x ': xs) ++ ys = x ': (xs ++ ys) 

type family Reverse xs where 
    Reverse '[] = '[] 
    Reverse (x ': xs) = Reverse xs ++ '[x] 

data HZipper xs where 
    HZipper :: HRec ys -> HRec zs -> HZipper (Reverse ys ++ zs) 

hcat :: HRec xs -> HRec ys -> HRec (xs ++ ys) 
hcat HNil   ys = ys 
hcat (HCons x xs) ys = HCons x (hcat xs ys) 

hreverse :: HRec xs -> HRec (Reverse xs) 
hreverse HNil   = HNil 
hreverse (HCons x xs) = hreverse xs `hcat` (HCons x HNil) 

catAssoc :: HRec xs -> Proxy ys -> Proxy zs -> (xs ++ (ys ++ zs)) :~: ((xs ++ ys) ++ zs) 
catAssoc HNil xs ys = Refl 
catAssoc (HCons x xs) ys zs = case catAssoc xs ys zs of 
    Refl -> Refl 

moveRight :: HZipper xs -> HZipper xs 
moveRight (HZipper ls HNil) = HZipper ls HNil 
moveRight (HZipper ls (HCons (x :: x) (xs :: HRec xs))) = 
    case catAssoc (hreverse ls) (Proxy :: Proxy '[x]) (Proxy :: Proxy xs) of 
    Refl -> HZipper (HCons x ls) xs 

還有第三種可能性，即增加一個存在邊界原Parts內部進行檢查，或有moveRight :: InBounds (S n) rs -> Parts n rs -> Parts (S n) rs，其中InBounds是界外球岬的證明。或者我們可以有InBounds (S n) rs => ...與InBounds類型家庭返回類約束。儘管如此，這種方法也需要相當多的證明。