如何使用符號創建類型級別列表以測試類型族

我嘗試瞭解Haskell類型級別編程。我寫了一個小功能來查找一個鍵，一個符號，在類型級別列表：如何使用符號創建類型級別列表以測試類型族

{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE PolyKinds #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE TypeOperators #-} 

import GHC.TypeLits 

type family Lookup (x :: k) (l :: [(k,v)]) :: k where 
    Lookup k ('(k,a) ': ls) = a 
    Lookup k ('(x,a) ': ls) = Lookup k ls 
    Lookup k '[]    = TypeError (Text "Key not found: ")

GHC（8.0.1）沒有錯誤編譯此功能，現在我需要測試在GHCI功能。在GHCI我設置的選項：

:set -XDataKinds 
:set -XTypeOperators

，並嘗試運行試驗例1：

:kind! Lookup "bar" '[("foo", Int), ("bar", String)]

字符串「酒吧」和「富」應該是類型層次絃樂又名Symbols。

GHC拒絕我的小測試案例有：

<interactive>:1:14: error: 
    • Expected kind ‘[(Symbol, v0)]’, 
     but ‘'[("foo", Int), ("bar", String)]’ has kind ‘[*]’ 
    • In the second argument of ‘Lookup’, namely 
     ‘'[("foo", Int), ("bar", String)]’ 
     In the type ‘Lookup "bar" '[("foo", Int), ("bar", String)]’

的問題是如何改變測試例子，所以GHC會接受它。

注：我的類型級別函數Lookup在它的第一個版本中，它可能是錯誤的，也許我應該使用CmpSymbol或做其他更改。但是，這是不是這個SO問題的主題。

來源

2017-07-12 Jogger

(k1, k2)是對類型的元素的類型/類和k2，和'(a, b)是類型級別對（注意'）。

'(a, b) :: (k1, k2) with a :: k1 and b :: k2

修復：

Lookup "bar" '[ '("foo", Int), '("bar", String)]

來源

2017-07-12 18:38:18

我只是去嘗試：你需要額外的空間' '['（...'，否則解析器解析字符文字... :) - 我隨意編輯相應。 – chi

哦，這個我很棘手：我認爲GHC會足夠聰明，知道在類型級別列表'[]中不能有值對，但只有類型級別對... – Jogger

如何使用符號創建類型級別列表以測試類型族

回答

相關問題