约束数据类型

Question

假设您有一个很好的归纳定义,并且您希望将其定义为Haskell中的数据类型.然而,你的归纳定义是(正如许多归纳定义所述)这样一种形式,即生成规则要求它们的"前提"具有某种结构.例如,假设我们有以下定义:

• 如果x是一个偶数,那么T x就是武器,
• 如果x是一个奇数,那么S x就是武器.

如果我想在Haskell中定义这个(作为单个)数据类型,我会写类似的东西

data Weapon =  T Int | S Int

显然,这是行不通的,你现在就可以生成T 5和S 4,例如.是否有一种自然的方式来传递对构造函数参数的限制,以便我可以编写类似于上面代码的东西来给出正确的定义？

Answer 1

这有点不是Haskelly,但在例如Agda中更为惯用:改变你的表示的解释,以便通过构造强制它是正确的.

在这种情况下,请注意if n :: Int,then even (2 * n)和odd (2 * n + 1).如果我们手动摆脱太大的情况Int,我们可以说在偶数Int和Ints 之间有一个双射; 奇数Int和Ints 之间的另一个.

所以使用这个,你可以选择这个表示:

data Weapon = T Int | S Int

并改变其解释,使得T n实际代表T (2 * n)的值和值S n代表S (2 * n + 1).因此,无论n :: Int您选择什么,T n都将有效,因为您将其视为" T-of-2*n"值.

Answer 2

你最好的镜头不是导出T和S显式,但允许自定义构造函数:

module YourModule (Weapon, smartConstruct) where

data Weapon =  T Int | S Int

smartConstruct :: Int -> Weapon
smartConstruct x
    | even x     = T x
    | otherwise  = S x

现在,在导入时YourModule,用户将无法创建T并S显式,但仅限于您的smartConstruct功能.

Answer 3

如果你愿意限制自己使用Nats,并且可以使用合理的高级魔法,你可以使用GHC.TypeLits.

{-# LANGUAGE DataKinds, GADTs, TypeOperators, KindSignatures #-}

import GHC.TypeLits

data Weapon (n :: Nat) where
    Banana      :: n ~ (2 * m) => Weapon n
    PointyStick :: n ~ (2 * m + 1) => Weapon n

banana :: Weapon 2
banana = Banana

pointyStick :: Weapon 3
pointyStick = PointyStick

为自己尝试,它不会编译错误(奇数/偶数)数字.

编辑:更实际的可能是仙人掌的方法.