Mohl byste mi ukázat, jak v nějakém šikovném typovém systému vyjádřím/definuji typ Date ? Tedy typ, který říká, že únor může mět pouze 28dní a každej přestupnej 29, etc.
Například v Idrisu:
import Data.Fin
%default total
prestupnyRok : Nat -> Bool
prestupnyRok rok = delitelny 400 SIsNotZ || (delitelny 4 SIsNotZ && not (delitelny 100 SIsNotZ))
where
delitelny : (x:Nat) -> Not (x = 0) -> Bool
delitelny x nz = (modNatNZ rok x nz) == Z
pocetDnuVMesici : Nat -> Fin 12 -> Nat
pocetDnuVMesici rok mesic =
case finToInteger mesic of
0 => 31
1 => 28 + (if prestupnyRok rok then 1 else 0)
2 => 31
3 => 30
4 => 31
5 => 30
6 => 31
7 => 31
8 => 30
9 => 31
10 => 30
_ => 31
-- Mesice a dny jsou cislovany od nuly.
-- Napriklad 29. unora 2004 se zapise jako MkDatum 2004 28 1.
data Datum : Type where
MkDatum : (rok:Nat) -> (mesic:Fin 12) -> (den:Fin (pocetDnuVMesici rok mesic)) -> Datum
Výstup pro chybné datum
MkDatum 2003 1 28 (dny i měsíce jsou číslovány od 0) je
(input):1:18:When checking argument prf to function Data.Fin.fromInteger:
When using 28 as a literal for a Fin 28
28 is not strictly less than 28
pro správné datum
MkDatum 2004 1 28MkDatum (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (fromIntegerNat 1903))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(FS FZ)
(FS (FS (FS (FS (FS (FS (FS (FS (FS (FS (FS (FS (FS (FS (FS (FS (FS (FS (FS (FS (FS (FS (FS (FS (FS (FS (FS (FS FZ)))))))))))))))))))))))))))) : Datum