小编Pat*_*wne的帖子

关于清单1,需要类型级别公理

(t a) = (t (getUI(t a)))

应该可以推导出每个特定类型类实例的定理.

test函数的编译是否证明了程序中特定类型的类型级别公理？编译是否免费提供了一个定理的例子!？

清单1

{-# LANGUAGE MultiParamTypeClasses #-}
data Continuant a = Continuant a  deriving (Show,Eq)

class UI a where

instance UI Int where

class Category t a where
   getUI :: (UI a) => (t a) -> a

 instance Category Continuant Int where
    getUI (Continuant a) = a

 -- axiom (t a) = (t (getUI(t a))) holds for given types?
 test :: Int -> Bool …

据我所知，Haskell 中的代数数据类型可以有两种形式，即和（例如data Bool = True | False）或乘积（例如data Pair = P Int Double）。以下是一些具有空值和一元值构造函数的数据类型。

data Z  = Z
data S n = S n  -- I think that this is a singleton type?
data S = S Int

这些类型是否被视为代数数据类型？如果是的话，他们叫什么？