如何在计算日期时正确处理Fin n和Integer？-Java 学习之路

在我探索伊德里斯的旅程中，我试图以“惯用”的方式编写一个小日期处理模块 . 这是我到目前为止所拥有的 .

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

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中使用期望类型Date检查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 的非整体性，而 isLeapYear 本身来自 mod 类型的非全部性 .

1 回答

1
嗯，这并不是那么微不足道，因为Idris需要你在每一步都得到证明，特别是如果你使用的是依赖类型 . 所有基本想法都已写在这个问题中：

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

我可能是阿格达（Agda）给伊德里斯 . 此外，我做了一些调整，以使您的代码总和 .

首先， 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 . 当您使用依赖类型时，此函数实际上非常复杂 . 正如您所注意到的，您有几种情况 . 例如：总和适合当月，总和下个月，总和跳过几个月，总和去年 . 每个这样的案件都需要证明 . 如果您想确保总和适合当月，您应该提供该事实的证明 .

在我转到代码之前，我想警告你，甚至编写日期库的非类型版本是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 的数值运算非常有限 . 所以你甚至可能很难添加两个 Nat 并使用给定的证明将它们转换为 Fin . 再次，写这样的东西比看起来更难:)

以下是代码的完整草图：http://lpaste.net/3314444314070745088
回复于 2024-04-29T16:50:49+08:00

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

1 回答

相关问题