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

Question

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

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

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检查addDays Date.case块的右侧：92：11与期望的类型 日期

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

嗯，这并不是很微不足道，因为伊德里斯要求你在每一步的证明，特别是如果你使用依赖类型。所有的基本思路已经写在了这个问题：

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

我会评论你的实现和翻译在回答代码（这可能阿格达）至伊德里斯。此外，我做了一些调整，使您的代码总数。

首先，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 

那么，与Fin数值操作根据Data.Fin module目前的状态非常有限。因此，即使增加两个Nat s并使用给定的证明将它们转换为Fin，您也可能会遇到困难。同样，写这样的东西是很难似乎比:)

这里是代码的全素描：http://lpaste.net/3314444314070745088