tjk*_*k42 6 haskell type-families
我对 haskell 中的类型级编程很陌生,并且我坚持使用以下示例。它是小型 dsl 的类型级别类型检查器的片段。我希望Find
类型族返回给定元素包含在 中的证明Env
,否则强制编译时错误。
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
import GHC.TypeLits
-- atomic data types in the source language
data Atom = Boolean
-- the typechecking environment
type Env = [(Symbol, Atom)]
-- A proof that a particular pair has been declared in the Env
data Elem (n :: Symbol) (a :: Atom) (e :: Env) where
DH :: Elem n a ('(n,a):e)
DT :: Elem n a e -> Elem n a (t:e)
-- Compile time type env lookup
type Find :: Symbol -> Atom -> Env -> Elem n a e
type family Find n a e where
Find n a ('(n,a): e) = DH
Find n a ('(t,p): e) = DT (Find n a e)
Find n a '[] = TypeError (Text "name '" :<>: Text n :<>: Text "' not found in env")
Run Code Online (Sandbox Code Playgroud)
然而,当我尝试Find
在 ghci 中评估时,它似乎被卡住了:
kind! Find "hi" Boolean '[ '("hi", Boolean) ]
Find "hi" Boolean '[ '("hi", Boolean) ] :: Elem n a e
Run Code Online (Sandbox Code Playgroud)
我预计这会减少到DH :: Elem "hi" Boolean '[ '("hi", Boolean) ]
,但似乎什么也没有发生。我是否以某种方式错误地定义了我的类型系列?