在运行时动态生成Haskell类型？

Question

能否在运行时根据给定的模板定义Haskell类型？我指的是以下情况。假设我需要一个整数类型，它的取值范围在编译时未知。我还想要一个特性：

succ 0 = 1
succ 1 = 2
...
succ n = 0

n 在编译时是未知的。我可以这样做：

data WrapInt = WrapInt {
        value       :: Int,
        boundary    :: Int
}

wrapInt :: Int -> Int -> WrapInt
wrapInt boundary value = WrapInt value boundary

现在我想要的是保留wrapInt函数，但避免将边界作为值存储在WrapInt类型内。相反，我希望它以某种方式存储在类型定义中，这当然意味着该类型必须在运行时动态定义。

在Haskell中是否有可能实现这一点？

- Sventimir

---

你必须将这个限制条件存储在某个地方。如果它不是在编译时就已知，那么它必须在运行时存在，可以作为结构体的一个成员或作为函数的参数传递进来。 - András Kovács

是的，那正是我想要的。 - Sventimir

你可能正在寻找有限集合（也见这里）。我之前写过一些解释，其中涉及到它们。 - effectfully

使用案例很简单：我需要一个类似于整数的类型，其中succ n = 0对于某个未知的编译时值n成立。它将用作计数器，我希望能够无惧地增加它，而不必检查是否超出范围。我不喜欢在值内部存储边界，因为它实际上是整个类型的属性。尽管我知道这在Haskell中无法完成，但我会看一下有限集合的事情。谢谢。 - Sventimir

考虑到因为该类型将在运行时创建，可能会有多个（不同值的n）。 因此逻辑上，每个包装的int都需要包含一些信息，以识别它实际上是成员的哪种类型，以便对其进行的操作可以使用正确的类型实现。那个“Boundary”字段不就是这种类型信息吗？ 您可以创建另一个表示“类型”的数据类型，并使每个WrapInt而是存储对其“类型对象”的引用... 但是，WrapIntType应包含什么数据？ 正是“Boundary”值！ - Ben

Answer 1

reflection包允许您在运行时生成新的“本地”类型实例。

例如，假设我们有以下可以“环绕”的值的类型类：

{-# LANGUAGE Rank2Types, FlexibleContexts, UndecidableInstances #-}

import Data.Reflection
import Data.Proxy

class Wrappy w where
   succWrappy :: w -> w

我们定义了一个携带虚类型参数的新类型：

data WrapInt s = WrapInt { getValue :: Int } deriving Show

使其成为 Wrappy 的一个实例:

instance Reifies s Int => Wrappy (WrapInt s) where
    succWrappy w@(WrapInt i) = 
        let bound = reflect w 
        in
        if i == bound
            then WrapInt 0
            else WrapInt (succ i)

有趣的部分是Reifies s Int约束。它的意思是：“幻象类型s在类型级别上表示类型为Int的值”。用户不会为Reifies定义实例，这是由reflection包的内部机制完成的。

因此，Reifies s Int => Wrappy (WrapInt s)的意思是：“每当s表示Int类型的值时，我们可以使WrapInt s成为Wrappy的一个实例”。 reflect函数接受与幻象类型匹配的代理值，并返回一个实际的Int值，该值在实现Wrappy实例时使用。

为了实际“分配”一个值给幻影类型，我们使用reify：

-- Auxiliary function to convice the compiler that
-- the phantom type in WrapInt is the same as the one in the proxy
likeProxy :: Proxy s -> WrapInt s -> WrapInt s
likeProxy _ = id

main :: IO ()
main = print $ reify 5 $ \proxy -> 
    getValue $ succWrappy (likeProxy proxy (WrapInt 5))

注意，reify的签名禁止幽灵类型从回调中逃逸，这就是为什么我们必须使用getValue解包结果的原因。

在这个答案中或反射GitHub存储库中可以查看更多示例。

- danidiaz

---

这正是我正在寻找的。谢谢！ - Sventimir

“reify (a :: k)” 真是太神奇了！首先，在幕后它是使用 “unsafeCoerce” 实现的 - 我没有看到其他方法。实现的想法是，为了满足要求，我们必须知道某个类型 s，使得 reflect (Proxy :: Proxy s) = a。当然，这是不可能的。但是如果这样的 s 存在，我们可以找到一个运行时表示 Reifies s k 的方式 - 它毕竟只是 proxy s -> k。const a 符合要求，并被不安全地转换到位。由于 s 是存在量化的，所以它并不重要，不能逃脱，与 ST s 相比较。 - WorldSEnder

Answer 2

这并非不可能，只是很丑陋。我们需要自然数。

data Nat = Z | S Nat

以及有界自然数

data Bounded (n :: Nat) where
    BZ :: Bounded n
    BS :: Bounded n -> Bounded (S n)

那么您的函数应该类似于：

succ :: Bounded n -> Bounded n
succ bn = fromMaybe BZ $ go bn where
    go :: Bounded n -> Maybe (Bounded n)
    go = ...

在go中，我们需要：

1. 如果n为Z（即如果Bounded达到了其最大值并溢出），则将BZ映射为Nothing
2. 如果n不是Z（即如果Bounded没有达到其最大值），则将BZ映射为Just (BS BZ)
3. 对于BS的情况，递归调用go

然而问题在于，无法在值级别上获取n。Haskell并不依赖于此。通常的方法是使用singletons。手动编写如下：

data Natty (n :: Nat) where
    Zy :: Natty Z
    Sy :: Natty n -> Natty (S n)

class NATTY (n :: Nat) where
    natty :: Natty n

instance NATTY Z where
    natty = Zy

instance NATTY n => NATTY (S n) where
    natty = Sy natty

现在我们可以在 go 中使用 Bounded n 来获取 n 的值级表示：

succ :: NATTY n => Bounded n -> Bounded n
succ bn = fromMaybe BZ $ go natty bn where
    go :: Natty n -> Bounded n -> Maybe (Bounded n)
    go  Zy      BZ     = Nothing
    go (Sy ny)  BZ     = Just (BS BZ)
    go (Sy ny) (BS bn) = BS <$> go ny bn

而 NATTY 类型类用于自动推断此值。

一些测试：

instance Eq (Bounded n) where
    BZ    == BZ    = True
    BS bn == BS bm = bn == bm
    _     == _     = False

zero :: Bounded (S (S Z))
zero = BZ

one :: Bounded (S (S Z))
one = BS BZ

two :: Bounded (S (S Z))
two = BS (BS BZ)

main = do
    print $ succ zero == zero -- False
    print $ succ zero == one  -- True
    print $ succ one  == two  -- True
    print $ succ two  == zero -- True

以下是需要翻译的内容：

代码。

---

使用singletons库，我们可以定义succ如下：

$(singletons [d| data Nat = Z | S Nat deriving (Eq, Show) |])

data Bounded n where
    BZ :: Bounded n
    BS :: Bounded n -> Bounded (S n)

succ :: SingI n => Bounded n -> Bounded n
succ bn = fromMaybe BZ $ go sing bn where
    go :: Sing n -> Bounded n -> Maybe (Bounded n)
    go  SZ      BZ     = Nothing
    go (SS ny)  BZ     = Just (BS BZ)
    go (SS ny) (BS bn) = BS <$> go ny bn

关于将运行时内容提升到类型级别，有两种方法：CPS和存在类型。

- effectfully

---

我不禁想知道一些良好的签名是否会使这看起来不那么神秘。 - dfeuer

@dfeuer，我使用了DataKinds扩展，它允许将数据类型视为种类，因此一切（Bounded，Natty和NATTY）都接收一个Nat。《Hasochism》论文正确描述了Haskell中的依赖类型编程。pigworker在这里也给出了很好的解释。 - effectfully

我只是建议如果您将Nat类型中的所有内容都添加上种类签名，那么代码可能会更易于阅读。 - dfeuer

非常感谢您详尽的回答。但是现在我想起来，Ben 在我的初始帖子下面写的很对。将边界存储在值级别上并不是很符合我的口味，但这是一个更简单的解决方案，所以我会采用它。但是我仍然需要分析这些东西，以便学习一些新知识。再次感谢。 - Sventimir

@dfeuer，好的，我已经添加了它们。 - effectfully

@Sventimir，不用谢。我理解你的选择：即使在一个正确类型化的语言中，这个解决方案可能也过于复杂了。在Haskell中，你很快就会遇到这样一种情况：你需要使用TypeFamilies，启用UndecidableInstances，然后猜测GHC能做什么，不能做什么。 - effectfully