Estoy interesado en los idiomas mecanografiados de forma dependiente. Los números finitos me parecen muy útiles. Por ejemplo, para indexar con seguridad matrices de tamaño fijo. Pero la definición no está clara para mí.

El tipo de datos para números finitos en Idris puede ser el siguiente: (Y probablemente similar en Agda)

data FiniteNum : Natural -> Type where
  FZero : FiniteNum (Succ k)
  FSucc : FiniteNum k -> FiniteNum (Succ k)

Y parece funcionar:

exampleFN : FiniteNum (Succ (Succ Zero))
exampleFN = FSucc FZero -- typechecks
-- exampleFN = FSucc (FSucc FZero)  -- won't typecheck

Pero, ¿cómo funciona esto? ¿Qué significa k? ¿Y por qué el comprobador de tipos acepta la primera implementación y rechaza la segunda?