haskell - 有没有什么方法可以限制ADT数据，使得只有有效的数据才能被构造？

Question

当我想定义Integer时，我尝试了这个

data Int = Pos Nat | Neg Nat
data Nat = Zero | Succ Nat

但是写完上面的代码后，我发现Pos Zero和Neg Zero都是可以构造出来的，这是我没有想到的。

当我想定义Rational时，同样的问题再次出现

data Rational = Rational Int Int 

我期望对于任何Rational n m，它应该满足m > 0 && gcd n m == 1

但我不知道如何确保我的 ADT 数据满足这些属性。因此，当我编写一些将其作为输入处理的函数时，我必须考虑这些非法情况。 我希望有某种方法可以在定义 ADT 时定义一次属性，而不是每次使用时都检查属性。

Answer 1

对于整数来说，这非常简单:

data Nat = Zero | Positive Pos
data Pos = One | Succ Pos
data Int = Pos Nat | Neg Pos

或者，您也可以继续使用Int = Pos Nat | Neg Nat 但将 Neg n 解释为表示 -(n+1) 而不是 -n，因此“- 0”是不可能的。

对于理性来说，这更加棘手。我认为通常最好的做法是让这些非标准化值在实现上可行，但在语义上仅考虑这些值的等价类，或者使用智能构造函数对它们进行标准化。这当然是 Rational 的方法需要。
可以限制定义，使得每个等价类只存在一个代表。这是how Agda defines the rationals:

record ℚ : Set where
  field
    numerator     : ℤ
    denominator-1 : ℕ
    isCoprime     : True (C.coprime? ∣ numerator ∣ (suc denominator-1))

  denominator : ℤ
  denominator = + suc denominator-1

  coprime : Coprime numerator denominator
  coprime = toWitness isCoprime

所以，它基本上只是在其依赖类型系统中编码 gcd ≠ 1 条件。拥有这样一个类型系统的人很幸运......

我不知道这样的定义可以如何翻译成 Haskell。 无论如何应该是可能的，但我怀疑它是否可行。

一个肯定有效但可能效率很低的解决方案是 enumerate all rational numbers ，然后仅将该枚举的索引存储为单个 Nat。或者更确切地说，实现所有积极理性的 Calkin-Wilf 树:

data PosRational = UnitRatio
                 | RatSucc PosRational
                 | RecipSucc PosRational

有趣的是如何为此定义 Num 等实例。让我们看看...

instance Fractional PosRational where
  recip UnitRatio = UnitRatio
  recip (RecipSucc x) = RatSucc $ recip x
  recip (RatSucc x) = RecipSucc $ recip x

instance Num PosRational where
  UnitRatio + x = RatSucc x
  x + UnitRatio = RatSucc x
  RatSucc x + y = RatSucc $ x + y
  x + RatSucc y = RatSucc $ x + y
  RecipSucc (RecipSucc x) + RecipSucc (RecipSucc y)
   -- = recip (1 + 1 + x) + recip (1 + 1 + y)
   -- = (2+y + 2+x) / ((2+x)*(2+y))
   -- = (4 + x + y) / (4 + 2*x + 2*y + x*y)
   -- = 1 / (1 + (x+y+x*y)/(4+x+y))
      = RecipSucc $ (4+x+y)/(x+y+x*y)
  RecipSucc (RatSucc x) + RecipSucc (RatSucc y)
   -- = recip (1 + recip (1+x)) + recip (1 + recip (1+y))
   -- = (1+x) / (1+x + 1) + (1+y) / (1+y + 1)
   -- = ((1+x)*(2+y)+(1+y)*(2+x)) / ((2+x)*(2+y))
   -- = (2+2*x+y+x*y + 2+x+2*y+x*y) / (4+2*x+2*y+x*y)
   -- = (4 + 3*x + 3*y + 2*x*y) / (4+2*x+2*y+x*y)
   -- = (4+2*x+2*y+x*y + x+y+x*y) / (4+2*x+2*y+x*y)
   -- = 1 + (x+y+x*y) / (4+2*x+2*y+x*y)
   -- = 1 + 1 / (1 + (4+x+y)/(x+y+x*y))
      = RatSucc . RecipSucc $ (4+x+y)/(x+y+x*y)
  ...