如何使用符号创建类型级别列表以测试类型族

我尝试了解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

如何使用符号创建类型级别列表以测试类型族

回答

相关问题