使用 Nat 的代数数据类型（单例库）答案

【问题标题】：Algebraic Data Types using Nat (singleton library)使用 Nat 的代数数据类型（单例库）
【发布时间】：2018-02-13 21:46:46
【问题描述】：

我一直在尝试声明一个代数数据类型以使用单例库在类型级别上进行操作。如果我不在构造函数中使用Nat、Symbol、Integer 或String，我可以毫不费力地做到这一点。例如：

{-# LANGUAGE GADTs                #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TemplateHaskell      #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeInType           #-}

import           Data.Singletons
import           Data.Singletons.TH

$(singletons [d|
  data Dim where
    NS :: Dim -- no size
    D  :: Bool -> Dim
   deriving (Eq, Show)
  |])

main :: IO ()
main = do
  let b = case toSing (D True) of
            (SomeSing d) -> show $ fromSing d
  putStrLn b

但如果我将Bool 更改为Nat 或Integer，它会失败。

如何定义代数数据类型以与在类型级别采用 Nat 或 Integer 的构造函数一起使用？

【问题讨论】：

标签： haskell gadt singleton-type

【解决方案1】：

从 README 中我了解到这是不可能的，因为 Nat 的特殊状态，但它也链接到可能的解决方法（请参阅下面 Github 问题中的最后一条评论）：将 Nat 包装在一些数据类型中单例可以处理。

https://github.com/goldfirere/singletons/issues/76

【讨论】：