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

Question

感谢本杰明·霍奇森（Benjamin Hodgson），我已经开始实现一个类型安全的sql-interface，在此stackoverflow问题中开始。

正如建议的那样，我已经开始阅读Singleton纸。我发现看到工作代码很有帮助，并努力查看提供的代码工作。但是，该代码已有三年历史，需要进行一些更新。伟大的！现在我可以学习一些东西。这是第一步，用类型文字字符串删除升级的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的表现仍然不佳。问题在于他们缺乏类似弦乐的行为（例如能够提取字符或从字符中制作字符串）。我相信最好的解决方案仍然是重新亮相的角色之一。