如何将列表与 Haskell 单例库一起使用

Question

我正在尝试使用使用列表的singletons库创建一个类型：

import Data.Singletons.TH (singletons)
$(singletons [d|
    data LLVMType
        = IntegerType
        | FloatType
        | FunctionType { argumentTypes :: [LLVMType] }
    |])
foo :: SLLVMType ('FunctionType '[ 'IntegerType ])
foo = ???

我试图使foo成为：SFunctionType [SIntegerType]，但是它会导致此错误：

• Couldn't match expected type ‘Data.Singletons.Sing '['IntegerType]’
              with actual type ‘[Data.Singletons.Sing 'IntegerType]’
• In the first argument of ‘SFunctionType’, namely ‘[SIntegerType]’
  In the expression: SFunctionType [SIntegerType]
  In an equation for ‘foo’: foo = SFunctionType [SIntegerType]

如何为类型检查foo创建表达式？或者我如何以另一种方式实现这一目标？

带有代码的 Github 存储库。

Answer 1

你非常接近，但你需要使用列表单例。

{-# language TemplateHaskell, DataKinds, GADTs, TypeFamilies #-}
module SingList where
import Data.Singletons.TH (singletons)
import Data.Singletons.Prelude.List (Sing (SNil, SCons))
$(singletons [d|
    data LLVMType
        = IntegerType
        | FloatType
        | FunctionType { argumentTypes :: [LLVMType] }
    |])
foo :: SLLVMType ('FunctionType '[ 'IntegerType ])
foo = SFunctionType (SCons SIntegerType SNil)