haskell - 如何证明可能的函数的个数？

Question

查看函数声明，例如:

myFoo :: Bool -> Bool

我可以说，函数myFoo有四种可能的唯一实现，因为函数类型是指数运算符，这是上面案例的证明2^2 = 4 :

myFoo1 :: Bool -> Bool
myFoo1 True = False 
myFoo1 True = True


myFoo2 :: Bool -> Bool
myFoo2 False = False 
myFoo2 False = True

我如何声明以下数据:

data Quad =
  One
  | Two
  | Three
  | Four
  deriving (Eq, Show)

和以下功能:

funcQuad :: Quad -> Quad

可能的实现是256(4^4)。我无法想象它，有很多实现。

如何在不写出来的情况下证明？

Answer 1

您可以使用代数来计算某种类型的居民数量。

有 3 种主要类型结构:

• 求和类型:要么 a b，写为 a + b
• 产品类型:(a, b)，写为a × b
• 指数(箭头)类型，a -> b，写为 b^a

还有一些基本类型，如单元类型()，写为1，空类型Void，写为0。

大多数常见代数都涉及类型(分布、交换性、幂等)。结果表达式的基本含义是您的类型的居民数量。平等可以翻译为类型世界中的同构。

对于像您这样的枚举(即无效构造函数的并集)，我们通常将其写为 1 + 1 + ... + 1 和 n 1s，给定 n 构造函数的数量。

在这里，您的 Quad 类型在类型上转换为 1 + 1 + 1 + 1，并且可以减少为 4。然后，您的 Quad -> Quad 类型将写为 4⁴，即 256。