如何系统地计算给定类型的居民数量？

Question

如何系统地计算系统F中给定类型的居民数量？

假设有以下限制:

• 所有居民终止,即没有底部.
• 所有居民都缺乏副作用.

例如(使用Haskell语法):

• Bool 有两个居民.
• (Bool, Bool) 有四个居民.
• Bool -> (Bool, Bool) 有十六个居民.
• forall a. a -> a 有一个居民.
• forall a. (a, a) -> (a, a) 有四个居民.
• forall a b. a -> b -> a 有一个居民.
• forall a. a 没有居民.

实现前三个算法是微不足道的,但我无法弄清楚如何为其他算法做到这一点.

Answer 1

我想解决同样的问题.以下讨论对我帮助很大:

滥用代数数据类型的代数 - 为什么这样做？

起初,我也受到诸如此类的困扰forall a. a -> a.然后,我有一个顿悟.我意识到的类型forall a. a -> a是莫根森-斯科特编码所述的单元类型.因此,它只有一个居民.同样,forall a. a是底部类型的Mogensen-Scott编码.因此,它没有居民.考虑以下代数数据类型:

data Bottom                         -- forall a. a

data Unit = Unit                    -- forall a. a -> a

data Bool = False | True            -- forall a. a -> a -> a

data Nat = Succ Nat | Zero          -- forall a. (a -> a) -> a -> a

data List a = Cons a (List a) | Nil -- forall a b. (a -> b -> b) -> b -> b

代数数据类型是一个总和的产品.我将使用语法???来表示该类型的居民数量?.我将在本文中使用两种类型:

1. 系统F数据类型,由以下BNF给出:

   ? = ?
     | ? -> ?
     | ? ?. ?
   

2. 代数数据类型,由以下BNF给出:

   ? = 
     | ?
     | ? + ?
     | ? * ?
     | ? ?. ?
   

计算代数数据类型的居民数量非常简单:

??       = 
??¹ + ?²? = ??¹? + ??²?
??¹ * ?²? = ??¹? * ??²?
?? ?. ??  = ?? [? ?. ? / ?]?

例如,考虑列表数据类型? ?. ? * ? + 1:

?? ?. ? * ? + 1? = ?(? * ? + 1) [? ?. ? * ? + 1 / ?]?
                 = ?? * (? ?. ? * ? + 1) + 1?
                 = ?? * (? ?. ? * ? + 1)? + ?1?
                 = ??? * ?? ?. ? * ? + 1? + ?1?
                 = ??? * ?? ?. ? * ? + 1? +  1

但是,计算System F数据类型的居民数量并不是那么简单.不过,它可以做到.为此,我们需要将System F数据类型转换为等效的代数数据类型.例如,System F数据类型? ?. ? ?. (? -> ? -> ?) -> ? -> ?等同于代数列表数据类型? ?. ? * ? + 1.

首先要注意的是,虽然System F类型? ?. ? ?. (? -> ? -> ?) -> ? -> ?有两个通用量词,但代数列表数据类型? ?. ? * ? + 1只有一个(定点)量词(即代数列表数据类型是单态的).

虽然我们可以使代数列表数据类型多态(即? ?. ? ?. ? * ? + 1)并添加规则?? ?. ?? = ? ?. ???但我们不这样做,因为它不必要地使问题复杂化.我们假设多态类型已经专门用于某些单形类型.

因此,第一步是删除除代表"定点"量词的那个之外的所有通用量词.例如,类型? ?. ? ?. ? -> ? -> ?变为? ?. ? -> ? -> ?.

由于Mogensen-Scott编码,大多数转换都很简单.例如:

? ?. ?                       = ? ?. 0                   -- bottom type

? ?. ? -> ?                  = ? ?. 1 + 0               -- unit type

? ?. ? -> ? -> ?             = ? ?. 1 + 1 + 0           -- boolean type

? ?. (? -> ?) -> ? -> ?      = ? ?. (? * 1) + 1 + 0     -- natural number type

? ?. (? -> ? -> ?) -> ? -> ? = ? ?. (? * ? * 1) + 1 + 0 -- list type

但是,有些转换不是那么简单.例如,? ?. ? -> ? -> ?不代表有效的Mogensen-Scott编码数据类型.不过,我们可以通过稍微处理这些类型来得到正确的答案:

?? ?. ? -> ? -> ?? = ?? -> ? ?. ? -> ??
                   = ?? ?. ? -> ?? ^ ??? 
                   = ?? ?. 1 + 0? ^ ??? 
                   = ?? ?. 1? ^ ??? 
                   = ?1? ^ ??? 
                   =  1 ^ ???
                   =  1

对于其他类型,我们需要使用一些技巧:

? ?. (?, ?) -> (?, ?) = (? ?. (?, ?) -> ?, ? ?. (?, ?) -> ?)
                      = (? ?. ? -> ? -> ?, ? ?. ? -> ? -> ?)

?? ?. ? -> ? -> ?? = ?? ?. 1 + 1 + 0?
                   = ?? ?. 2?
                   = ?2?
                   =  2

?? ?. (?, ?) -> (?, ?)? = ?? ?. ? -> ? -> ?? * ?? ?. ? -> ? -> ??
                        = 2 * 2
                        = 4

虽然有一个简单的算法可以给我们Mogensen-Scott编码类型的居民数量,但我想不出任何能给我们任何多态类型的居民数量的通用算法.

事实上,我有一种非常强烈的直觉,即通常计算任何多态类型的居民数量是一个不可判定的问题.因此,我认为没有任何算法可以为我们提供任何多态类型的居民数量.

不过,我相信使用Mogensen-Scott编码类型是一个很好的开始.希望这可以帮助.