8

我是 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（所以寻找答案也有点困难）......

4

5 回答 5

12

一般来说没有。这种东西称为子集类型，它是 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）。

于 2013-11-01T15:40:56.903 回答
6

不，类型系统需要支持细化类型（或完全依赖类型，如@jozefg 所建议的那样）。

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

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

于 2013-11-01T15:43:50.477 回答
1

将子集包装在新类型中

newtype EvenInteger = EvenInteger {
    unEvenInteger :: Integer
} deriving (Show, Eq, Ord, Num)

mkEvenInteger :: Integer -> Maybe EvenInteger
mkEvenInteger n = case n % 2 of
    0 -> Just $ EvenInteger n
    _ -> Nothing

squared :: EvenInteger -> EvenInteger
squared n = n * n
于 2013-11-01T16:07:47.207 回答
1

一种可能性是

newtype Even n = Even n
getEven (Even n) = 2*n

squared :: Num n => Even n -> Even n
squared (Even n) = Even (2*n*n)
于 2013-11-01T18:06:06.140 回答
1

正如其他地方所提到的，像 LiquidHaskell 中的细化类型可以表达这一点。这是它的样子：

module Evens where

{-@ type Even = {v:Int | v mod 2 = 0} @-}

{-@ square :: Even -> Int @-}
square :: Int -> Int
square n = n * n

-- calling the function:
yup = square 4
-- nope = square 3 -- will not compile if this is uncommented

您可以通过在此处插入来尝试一下：http ://goto.ucsd.edu:8090/index.html

于 2015-08-06T15:43:26.220 回答