Sto cercando un esempio (se esiste) di una definizione di una data in un linguaggio di programmazione (Idris, Coq, ecc.) con tipi dipendenti in cui tale definizione è coerente e sicura per tipo con cui intendo che l'espressione di data non valida o letterale darebbe un errore di tempo di compilazione. Se la definizione completa non è possibile quale sarebbe la migliore che si possa pensare?
Beh, non hai davvero bisogno di tipi dipendenti per modellare un mese ben formato,
data Month = January
| February
| March
...
| November
| December
Diventa leggermente più doloroso con il giorno e l'anno, poiché quelli sono piuttosto più grandi. In effetti, la rappresentazione legale di un giorno del mese dipende dal mese. Definiamo una funzione
numDays : Month -> Nat
numDays January = 31
...
numDays December = 31
Ora, quello che vogliamo dire è che Day è un tipo che impiega un mese e restituisce un nuovo tipo. Quindi
Day : Month -> Type
Day m = ...
dove ... dice in qualche modo "Sono un numero compreso tra 0 e numDays m ". Possiamo rappresentarlo con un tipo chiamato Fin
data Fin (n : Nat) : Type where
FinZ : Fin n
FinS : Fin m -> m + 1 < n -> Fin (m + 1)
In altre parole, Fin è tutti i numeri da 0 a n , escluso n .
Quindi ora possiamo dire
Day : Month -> Type
Day m = Fin (numDays m)
Come per anni, quelli sono indipendenti sia dal mese che dal giorno, lasciandoci con
data Date : Type where
mkDate : (year : Nat)(month : Month)(day : Day month) -> Date
Se volessimo essere precisi, potremmo avere day dipendente da year per tenere conto degli anni bisestili.
Se lavorassimo in Agda e avessimo la sintassi mix-fix. Per ottenere letterali tutto quello che dovremmo fare è dire
[_-_-_] : Nat -> (m : Month) -> Day m -> Date
[_-_-_] = mkDate
Potremmo fare qualcosa di simile con le notazioni di Coq.
Come mini esempio compilabile,
open import Data.Nat
open import Data.Fin
data Month : Set where
January : Month
February : Month
numDays : Month -> ℕ
numDays January = 31
numDays February = 28
Day : Month → Set
Day m = Fin (numDays m)
record Date : Set where
constructor mkDate
field
month : Month
day : Day month
_/_ : (m : Month)(n : ℕ){p : Data.Nat._≤_ (suc n) (numDays m)} → Date
_/_ m n {p} = mkDate m (inject≤ (fromℕ n) p)
Ora un altro modo ovvio per modellare date e ore è avere nozioni come un tempo assoluto e altre nozioni come una durata. Quindi possiamo combinare questi e produrre altri timestamp.
Quindi, per esempio, potremmo voler dire "5 secondi prima di 1 minuto dopo T". Il problema si presenta confrontando i tempi come questo per l'uguaglianza. Non ci interessa davvero la struttura interna precisa di come possiamo arrivare ad un punto nel tempo, solo che siamo arrivati lì. Quindi dobbiamo stare attenti a non lasciare che i nostri dati abbiano una struttura che potrebbe distinguere valori altrimenti equivalenti.
Questo è un problema davvero sottile e spinoso come risulta. Non c'è davvero un buon modo per affrontare questo in Idris o Coq poiché mancano di tipi di quoziente.
Leggi altre domande sui tag type-systems