使"单身人士论文"更新.如何使用singleton库实现AChar数据类型

Question

感谢Benjamin Hodgson,我已经开始实现一个类型安全的SQL-Interface,从这个 stackoverflow问题开始.

据我所知,我已经开始阅读单身纸.我发现看到工作代码有很多帮助,并努力查看提供的代码是否有效.但是,代码已有三年历史,需要进行一些更新.大!现在我开始学习一些东西.这是第一步,使用type-literal字符串删除提升类型的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这些仍然不能很好地发挥作用.问题是它们缺乏类似字符串的行为(比如能够从字符中提取字符或创建字符串).我相信最好的解决方案仍然是重新定义角色的丑陋.