计算日期时如何正确处理 Fin n 和 Integer？

Question

在探索 Idris 的过程中，我尝试以“惯用”的方式编写一个小型日期处理模块。这是我目前所拥有的。

首先我有一些基本类型来表示日、月和年：

module Date 

import Data.Fin

Day : Type
Day = Fin 32

data Month : Type where
  January    : Month
  February   : Month
  .... 

toNat : Month -> Nat
toNat January    = 1
toNat February   = 2
... 

data Year : Type where
  Y : Integer -> Year

record Date where
  constructor MkDate
  day   : Day
  month : Month 
  year  : Year

我想实现一个函数addDays 为Date 添加一些天数。为此我定义了以下辅助函数：

isLeapYear : Year -> Bool
isLeapYear (Y y) = 
  (((y `mod` 4) == 0) && ((y `mod` 100) /= 0)) || ((y `mod` 400) == 0) 

daysInMonth : Month -> Year -> Day
daysInMonth January _      = 31
daysInMonth February year  = if isLeapYear year then 29 else 28
daysInMonth March _        = 31
...

最后尝试将addDays 定义为：

addDays : Date -> Integer -> Date
addDays (MkDate d m y) days =
  let maxDays = daysInMonth m y
      shiftedDays = finToInteger d + days
  in case integerToFin shiftedDays (finToNat maxDays) of  
          Nothing => ?hole_1
          Just x  => MkDate x m y

我陷入了一个非常基本的情况，即增加的天数适合当前月份的持续时间。这是编译器的输出：

在 Date.idr:92:11 的 addDays 中使用预期类型检查 Date.case 块的右侧时 日期

 When checking argument day to constructor Date.MkDate:
         Type mismatch between
                 Fin (finToNat maxDays) (Type of x)
         and
                 Day (Expected type)

         Specifically:
                 Type mismatch between
                         finToNat maxDays
                 and
                         32

这很令人费解，因为maxDays 的类型显然应该是Day，也就是Fin 32。

我怀疑这可能与daysInMonth 的非全部有关，这源于isLeapYear 的非全部，而mod 类型的Integer 类型的非全部。

Answer 1

嗯，这不是那么简单，因为Idris 需要您在每一步都提供证明，尤其是在您使用依赖类型时。所有基本思想都已经写在这个问题中了：

Is there a way to define a consistent date in a dependent type language?

我会评论你的实现并将回答中的代码（可能是Agda）翻译成Idris。我还做了一些调整以使您的代码完整。

首先，Month 可以写得简单一点：

data Month = January
           | February
           | March

我不会写完所有的 12 个月，这只是一个例子。

第二，Year 类型应该存储Nat 而不是Integer，因为大多数与Integer 一起使用的函数并不完整。这样更好：

data Year : Type where
    Y : Nat -> Year

这有助于使isLeapYear 检查总数：

isLeapYear : Year -> Bool
isLeapYear (Y y) = check4 && check100 || check400
  where
    check4 : Bool
    check4 = modNatNZ y 4 SIsNotZ == 0

    check100 : Bool
    check100 = modNatNZ y 100 SIsNotZ /= 0

    check400 : Bool
    check400 = modNatNZ y 400 SIsNotZ == 0

接下来，将Day 设为Fin 32 并不好。最好具体指定每个月的天数。

daysInMonth : Month -> Year -> Nat
daysInMonth January  _    = 31
daysInMonth February year = if isLeapYear year then 29 else 28
daysInMonth March    _    = 31

Day : Month -> Year -> Type
Day m y = Fin (daysInMonth m y)

你应该稍微调整一下你的Date记录：

record Date where
    constructor MkDate
    year  : Year
    month : Month
    day   : Day month year

好吧，现在关于addDays。当您使用依赖类型时，此函数实际上非常复杂。正如您正确注意到的那样，您有几种情况。例如：sum 适合当月，sum 到下个月，sum 跳过几个月，sum 到年。每一个这样的案例都需要证明。如果您想确保该金额适合当月，您应该提供该事实的证明。

在开始编写代码之前，我想警告您，即使是日期库的非类型化版本也是increadibly hard。此外，我想没有人还没有尝试过使用某些具有依赖类型的语言来实现全功能版本。所以我的解决方案可能远非最好的。但至少应该给你一些关于你做错了什么的想法。

然后你可以开始写一些这样的函数：

daysMax : (d: Date) -> Nat
daysMax (MkDate y m _) = daysInMonth m y

addDaysSameMonth : (d : Date)
                -> (n : Nat)
                -> Prelude.Nat.LT (finToNat (day d) + n) (daysMax d)
                -> Date
addDaysSameMonth d n x = ?addDaysSameMonth_rhs

嗯，根据Data.Fin module 的当前状态，Fin 的数值运算非常有限。因此，即使添加两个Nats 并使用给定的证明将它们转换为Fin，您也可能会遇到困难。再说一次，写这样的东西比看起来更难:)

这里是完整的代码草图：http://lpaste.net/3314444314070745088