haskell - 如何根据 Haskell 中的输入值限制类型？

Question

我是 Haskell 的新手。对不起，如果这个问题有一个明显的答案。

我有

data Tmp = Foo Int
         | Bar Int
         | Baz Int

和

data Test = A Tmp Tmp

构造函数 A Tmp Tmp可以为 Tmp 采用任何构造函数除了 A (Baz i) (Baz j)在哪里 i和 j是任意的 Int s。有什么办法可以吗
限制第二个 Tmp在 A Tmp Tmp来自 Baz如果第一个 Tmp已经是 Baz ?

Answer 1

答案取决于您希望如何实现限制:在运行时或编译时。

在运行时强制执行限制 ，您可以添加一个函数(例如 makeA )来检查限制，然后调用构造函数。这种做一些事情然后调用构造函数的函数也称为智能构造函数。如果只导出智能构造函数makeA但不是真正的构造函数A从一个模块中，您可以确定其他模块使用智能构造函数，因此始终检查限制。

例子:

module Test (Tmp (Foo, Bar, Baz), Test (), makeA) where
  data Tmp
     = Foo Int
     | Bar Int
     | Baz Int

  data Test = A Tmp Tmp

  makeA :: Tmp -> Tmp -> Tmp
  makeA (Baz _) (Baz _) = error "makeA: two baz problem"
  makeA tmp1 tmp2 = A tmp1 tmp2

这种技术的好处是您根本不必更改数据类型。缺点是该限制仅在运行时强制执行。

在编译时强制执行限制 ，您需要以某种方式更改数据类型。当前数据类型的问题是类型检查器无法区分 Foo 构造的值。和 Bar和 Baz 构造的值.对于类型检查器，这些都是 Tmp值，因此类型检查器无法强制某些 Tmp值(value)观还可以，其他的不行。所以我们必须改变数据类型来编码 Tmp 的“Bazness”。类型中的值。

一种将 Bazness 编码为 类型的选项将重组 Tmp如下:

data TmpNotBaz
  = Foo Int
  | Bar Int

data Tmp
  = NotBaz TmpNotBaz
  | Baz Int

现在很清楚 TmpNotBaz 类型的值不能是 Baz , 但类型为 Tmp 的值可以是 Baz .这个想法的好处是它只使用了基本的 Haskell 特性。一个小缺点是您需要调用 NotBaz进入你的代码。一个主要缺点是我们仍然不能直接表达“ A 的一个参数可以是 Baz 如果另一个不是”的想法。我们将不得不编写 A 的多个版本:

data Test
  = A1 TmpNotBaz Tmp
  | A2 Tmp TmpNotBaz

现在我们可以通过选择 A1 来表达我们想要的所有值。或 A2根据需要，我们无法表达 A (Baz ...) (Baz ...)不再，根据需要。这个解决方案的一个问题是，过去有多种表示形式，例如， A (Foo 1) (Foo 2)。 : 两个 A1 (Foo 1) (NotBaz (Foo 2))和 A2 (NotBaz (Foo 1)) (Foo 2)表示这个值。

您可以尝试使用这样的数据类型的结构，并创建一个适合您情况的版本。

将 Bazness 编码为 类型的另一种选择将在 Tmp 中注释一些类型级别的信息。键入并使用类型级编程来推理此类型级信息。这个想法的缺点是它使用了更高级的 Haskell 特性。实际上，有很多新兴的方法可以做这种事情，目前还不清楚其中哪些最终会被认为是“标准”的高级 Haskell。也就是说，这是一种方法:

{-# LANGUAGE GADTs, TypeFamilies, DataKinds #-}

data Bazness = IsBaz | NotBaz

data BothBazOrNot = BothBaz | NotBothBaz

type family AreBothBaz (b1 :: Bazness) (b2 :: Bazness) :: BothBazOrNot where
  AreBothBaz 'IsBaz 'IsBaz = 'BothBaz
  AreBothBaz _ _ = 'NotBothBaz

data Tmp (b :: Bazness) :: * where
  Foo :: Int -> Tmp 'NotBaz
  Bar :: Int -> Tmp 'NotBaz
  Baz :: Int -> Tmp 'IsBaz

data Test where
  A :: AreBothBaz b1 b2 ~ 'NotBothBaz => Tmp b1 -> Tmp b2 -> Test

注意构造函数的类型签名 Foo , Bar和 Baz谈谈构造函数是否创建了 IsBaz或 NotBaz .以及 A 的类型签名如何谈一些 b1和 b2选择，以便 NotBothBaz .

使用此代码，我们可以编写以下表达式:

A (Foo 1) (Bar 2)

A (Foo 1) (Baz 2)

A (Baz 1) (Bar 2)

但是如果我们尝试写 A (Baz 1) (Baz 2) ，类型检查器提示:

Couldn't match type 'BothBaz with 'NotBothBaz
    arising from a use of A
 In the expression: A (Baz 1) (Baz 2)

所以类型检查器发现在这种情况下， A 的参数是 BothBaz , 但我们注释了 A 的类型只接受 NotBothBaz 的参数，所以类型检查器提示 BothBaz不同于 NotBothBaz .