haskell - 使 "The Singletons Paper"保持最新。如何使用单例库实现 AChar 数据类型

Question

感谢Benjamin Hodgson ，我已经开始实现类型安全的 SQL 接口(interface)，从 this 开始堆栈溢出问题。

按照建议，我已经开始阅读 the singleton paper 。我发现查看工作代码有很大帮助，并尽力查看提供的 code工作。然而，该代码已有三年历史，需要一些更新。伟大的!现在我要学点东西了。这是第一步，删除带有类型文字字符串的提升类型 AChar。

来自singletons-examples/DatabaseStar.hs中的原始代码

{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# Language PolyKinds, DataKinds, TemplateHaskell, TypeFamilies,
    GADTs, TypeOperators, RankNTypes, FlexibleContexts, UndecidableInstances,
    FlexibleInstances, ScopedTypeVariables, MultiParamTypeClasses #-}

module DatabaseStar where

import Data.Singletons
import Data.Singletons.CustomStar
import Data.Singletons.TH

$(singletons [d|
-- A re-definition of Char as an algebraic data type.
-- This is necessary to allow for promotion and type-level Strings.
  data AChar = CA | CB | CC | CD | CE | CF | CG | CH | CI
             | CJ | CK | CL | CM | CN | CO | CP | CQ | CR
             | CS | CT | CU | CV | CW | CX | CY | CZ
             deriving (Read, Show, Eq)

-- A named attribute in our database
  data Attribute a = Attr [AChar] a

-- A schema is an ordered list of named attributes
  data Schema a = Sch [Attribute a]
  |]

我发现 AChar 并不令人满意，并且很快意识到不再需要它。

但我不确定如何为此用例实现类型级Strings。有人可以提供链接供我调查和/或提示吗？

Answer 1

我相信类型级“字符串”已经存在 - 它们的名称为 Symbol .

ghci> :set +t -XTypeInType
ghci> import GHC.TypeLits
ghci> import Data.Proxy
ghci> Proxy :: Proxy "I'm a type level string!"
Proxy
it :: Proxy "I'm a type level string!"

也就是说，我认为 singleton 仍然不能很好地适应这些。问题在于它们缺乏类似字符串的行为(例如能够提取字符或从字符创建字符串)。我相信最好的解决方案仍然是重新声明字符这一丑陋的解决方案。