タイプファミリをテストするための記号付きのタイプレベルリストを作成する方法

Question

私は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の中の関数をテストする必要があります。

:set -XDataKinds 
:set -XTypeOperators 

と最初のテストの例を実行してみてください：文字列「バー」と「foo」がタイプレベルの文字列別名Symbolsでなければなりません

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

をGHCiの中で、私は、オプションを設定します。質問は、試験例を変更する方法なので、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の質問の話題です。

Answer 1

(k1, k2)タイプ/種類​​とk2の要素のペアの種類であり、そして'(a, b)型レベル対（'に注意）です。

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

修正：:) ...そうでない場合は、パーサはリテラル文字を解析し、 `...（ '['、`あなたは追加のスペースを必要とする - 私は：

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