類型級別列表上的平等約束

我試圖強制一個類型級別的約束，即類型級別列表必須與類型級別納稅人攜帶的長度相同。例如，使用從單例[1]包長度：類型級別列表上的平等約束

data (n ~ Length ls) => NumList (n :: Nat) (ls :: [*]) 

test :: Proxy (NumList 2 '[Bool, String, Int]) 
test = Proxy

我不希望這個代碼被編譯，因爲存在不匹配。

編輯：由於dfeuer提到數據類型上下文不是一個好主意。我能做到在價值層面的比較，但我希望能夠在類型級別要做到這一點：

class NumListLen a 
    sameLen :: Proxy a -> Bool 

instance (KnownNat n, KnownNat (Length m)) => NumListLen (NumList n m) where 
    sameLen = const $ (natVal (Proxy :: Proxy n)) == (natVal (Proxy :: Proxy (Length m)))

~~~~

編輯：八九不離十回答我自己的問題，只需添加約束到該實例：

class NumListLen a 
    sameLen :: Proxy a -> Bool 

instance (KnownNat n, KnownNat (Length m), n ~ Length m) => NumListLen (NumList n m) where 
    sameLen = const $ (natVal (Proxy :: Proxy n)) == (natVal (Proxy :: Proxy (Length m)))

/home/aistis/Projects/SingTest/SingTest/app/Main.hs:333:13: 
    Couldn't match type ‘3’ with ‘2’ 
    In the second argument of ‘($)’, namely ‘sameLen test’ 
    In a stmt of a 'do' block: print $ sameLen test 
    In the expression: 
     do { print $ sameLen test; 
      putStrLn "done!" }

[1] https://hackage.haskell.org/package/singletons-2.0.0.2/docs/Data-Promotion-Prelude-List.html#t:Length

來源

2016-01-13 sheganinans

這是一個數據類型上下文。數據類型上下文完全沒用。我懷疑你現在還不能完全按照Haskell的原則來做，但是單身人士可以做一些奇怪的事情...... – dfeuer

是的，你說得對，數據類型的背景並不完全如何會想要這樣做。但他們明白這一點。我能夠確定類型值並在值級別進行比較，但這不是我想要做的。 – sheganinans

你能否更好地解釋一下你的最終目標是什麼？你真的想表達什麼？ – dfeuer

一種選擇可能是使用類型系列：

data Nat = Z | S Nat 

type family LengthIs (n :: Nat) (xs :: [*]) :: Bool where 
    LengthIs 'Z '[] = 'True 
    LengthIs ('S n) (x ': xs) = LengthIs n xs 
    LengthIs n xs = 'False 

test :: LengthIs ('S ('S 'Z)) '[Bool,String,Int] ~ 'True =>() 
test =()

這不會通過類型檢查器;使其通過的唯一方法是使類型列表具有兩個元素。我不知道Nat如何在singletons庫中工作，但我想你可能能夠做類似的事情。

來源

2016-01-13 04:39:01 dfeuer

很好的例子，但我想用GHC的內建類型的nats。另外我回答了我自己的問題！ – sheganinans

如果這有點像一個不變（這好像是），你應該存儲在數據類型的證明：

{-# LANGUAGE PolyKinds, UndecidableInstances #-} 

import GHC.TypeLits 

type family Length (xs :: [k]) :: Nat where 
    Length '[] = 0 
    Length (x ': xs) = 1 + Length xs 

data TList n l where 
    TList :: (Length xs ~ n) => TList n xs

注意，儘管證明仍然可以在類型級別，它是數據構造函數背後的某種「隱藏」。你可以簡單地通過模式匹配收回證明：

data (:~:) a b where Refl :: a :~: a 

test :: TList n l -> Length l :~: n 
test TList = Refl

如今，這兩個參數之間的不匹配是一種錯誤：

bad :: TList 3 '[Int, Bool] 
bad = TList 

good :: TList 2 '[Int, Bool] 
good = TList

當然，這一點仍然可以通過谷值被打，所以

uh_oh :: TList 10 '[] 
uh_oh = undefined

爲了避免這種情況，只需確保您始終在構造函數TList上匹配模式。

來源

2016-01-13 08:21:20 user2407038

非常好，這與我正在尋找的東西非常接近！儘管如何使用Proxy來完成這項工作？ – sheganinans

是的，我想繼續這個不變。但我不想定義一個單獨的TList，它應該使用Proxy。 – sheganinans

不可能 - 「代理」的整個點是它沒有類型信息。我無法確切知道爲什麼您需要特別使用代理服務器 - 無論如何，您始終可以生成「代理服務器」。你當然可以簡單地把約束放在你需要的地方，並在那裏使用'Proxy'：'Length xs〜n => Proxy xs - > Proxy n - > ...'但是你沒有「通過構造來修正「財產。 – user2407038

類型級別列表上的平等約束

回答

相關問題