parametricity-proofs:多态函数居民数量的证明

参数证明 通过同构到代数数据类型证明多态函数的居民数量。 例如，我们证明id :: a -> a通过()的iso具有一个居民。 对于(.) :: (b -> c) -> (a -> b) -> a -> c 。 一个超酷的结果是，如果您使用证明的倒数部分来生成原始函数，即apply () -> (forall ab c. (b -> c) -> (a -> b) -> a -> c)到() ，GHC将融合中间步骤，您将获得(.)的实际定义。 基于