Haskell 类型级别约束

Question

我很好奇是否可以在 Haskell 中编写这样的（伪代码）：

data Clock = Clock {hour :: (0 <= Int <= 24),  minutes :: (0 <= Int <= 60)}

使（在类型级别）无法创建如下内容：

let a = Clock 34 236

或者应该使用一种时钟构建器来检查并创建有效的时钟时间？

Answer 1

具体的例子最好用来自模块化算术包的类型来表达：

{-# LANGUAGE TypeOperators, TypeFamilies, DataKinds #-}

import Data.Modular

data Clock = Clock {hour :: Int/24,  minutes :: Int/60}

请注意，这里的上限是唯一的，因为您的代码中也应该有。

模算术是商类型的一种特殊情况，在某些方面比受约束更实用。类型。但是 Haskell 对两者都没有普遍的、直接的支持。正如 Willem Van Onsen 提到的，Liquid Haskell 添加了这样的功能。不能说太多，但我多次听说它的效果非常好。

Answer 2

智能构造器

一种简单的方法是使用智能封装和智能构造函数：

module HoursAndMinutes (Hours, mkHours, getHours, Minutes, mkMinutes, getMinutes) where

newtype Hours = UnsafeHours Int

mkHours :: Int -> Maybe Hours
mkHours n | 0 <= n && n < 24 = Just (UnsafeHours n)
          | otherwise = Nothing

getHours :: Hours -> Int
getHours (UnsafeHours n) = n

newtype Minutes = UnsafeMinutes Int

mkMinutes :: Int -> Maybe Minutes
mkMinutes n | 0 <= n && n < 60 = Just (UnsafeMinutes n)
            | otherwise = Nothing

getMinutes :: Minutes -> Int
getMinutes (UnsafeMinutes n) = n

现在在您的其他代码中，如果您导入，HoursAndMinutes则无法构造 invalidHours或Minutes.

data Clock = Clock {hours :: Hours,  minutes :: Minutes}

那么这将导致Nothing：

Clock <$> mkHours 34 <*> mkMinutes 236

精制

您可以使用包中的内置谓词refined来稍微简化此方法：

Clock <$> mkHours 34 <*> mkMinutes 236

然后你可以构建一个：

Clock <$> refine 34 <*> refine 236

这将是Left (RefineSomeException ...)。

缺点仍然是检查是在运行时进行的。您可以使用 Template Haskell 进行编译时检查：

Clock $$(refineTH 34) $$(refineTH 236)

这将在编译时抛出异常。

液体哈斯克尔

正如 Willem van Onsem 在评论中所建议的那样，您可以通过使用Liquid Haskell使这更方便：

data Clock = Clock
  { hours   :: Refined (FromTo 0 23) Int
  , minutes :: Refined (FromTo 0 59) Int
  }

在这里尝试一下。