Una definizione per set finiti in Agda

Question

Sono nuovo di Agda. Sto leggendo il giornale "Tipi dipendenti al lavoro" di Ana Bove e Peter Dybjer. Non capisco la discussione sui set finiti (a pagina 15 nella mia copia).

Il documento definisce un tipo Fin:

data Fin : Nat -> Set where 
    fzero : {n : Nat} -> Fin (succ n) 
    fsucc : {n : Nat} -> Fin n -> Fin (succ n) 

Devo mancare qualcosa di ovvio. Non capisco come funzioni questa definizione. Qualcuno potrebbe semplicemente tradurre la definizione di Fin nell'inglese quotidiano? Potrebbe essere tutto ciò di cui ho bisogno per capire questa parte del documento.

Grazie per aver trovato il tempo di leggere la mia domanda. Lo apprezzo.

Answer 1

data Fin : Nat -> Set where 

Fin è un tipo di dati parametrizzata un numero naturale (o: Fin è una funzione del tipo di livello che prende una Nat e restituisce un (tipo base Set), cioè per qualsiasi numero naturale nFin n è un Set).

fzero : {n : Nat} -> Fin (succ n) 

Per tutti i numeri naturali nfzero è un membro del tipo/set Fin (succ n) (da cui deriva che per tutti i numeri positivi (cioè tutti naturali eccetto zero) nfzero è un membro della Fin n).

fsucc : {n : Nat} -> Fin n -> Fin (succ n) 

Per tutti i numeri naturali n e tutti i valori m di tipo Fin n, fsucc m è un membro di tipo Fin (succ n).

---

Quindi fzero è un membro della Fin n per tutti n tranne zero e fsucc m è un membro di Fin n per tutti n che rappresentano un numero maggiore di fsucc m.

Fondamentalmente Fin n rappresenta il Set di tutti i numeri naturali inferiori a n, cioè di tutti gli indici validi per gli elenchi di dimensioni n.