是否可以在现有类型的子集上定义函数？

Question

我是Haskell的新手,想知道是否可以定义一个仅在已有类型的子集上定义的函数,而不必实际定义新类型.

示例:我想创建一个只接受整数(甚至是自然数等)的函数并返回,例如,这个数字的平方,如:

squared :: 2*Integer -> Integer
squared n = n*n

当然,以上两行不起作用.

我知道我可以这样写:

squared' :: Integer -> Integer
squared' n 
  | (even n) = n*n
  | otherwise = error "n is not even!"

或类似的东西,但我想知道是否有可能像非工作示例这样的东西.

我希望这个问题不是完全愚蠢的(或者已经回答过了)但是我真的不知道很多Haskell(所以寻找答案也有点困难)......

Answer 1

一般没有.这样的事情被称为子集类型,它是Haskell没有的依赖类型的标志.通常它通过使用证明该值满足某些属性的值来实现,但由于我们在Haskell中没有证明概念,因此我们陷入困境.

通常伪造它的方式是"智能构造函数".

newtype Even = Even {unEven :: Integer} deriving (Eq, Show, Ord)

toEven :: Integer -> Maybe Even
toEven a | even a = Just $ Even a
         | otherwise = Nothing

然后隐藏Even构造函数.

如果你真的想要它,你可以切换到一种语言,它可以与具有依赖类型的Haskell互操作(考虑到Coq和Agda).

Answer 2

不可以.类型系统需要支持细化类型(或完全依赖类型,如@jozefg所示).

这是一个带有细化类型的Haskell扩展.

http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/01/01/refinement-types-101.lhs/