[Práctico 3] Ej: 8

[Práctico 3] Ej: 8

de Lia Malvarez Busquets -
Número de respuestas: 2

Buenas! No termino de entender la estructura de ArrayNat/Array del ejercicio 8. 

Mi primera intuición fue que el natural que recibe dicho Parameter represente el largo (por eso empty sería ArrayNat 0), pero luego, el tener que realizar un array con determinados elementos en él, me hizo dudar dicha conjetura, no entiendo cómo se podrían determinar los elementos del arreglo.

A su vez, ¿Cómo es posible parametrizar el tipo de los elementos internos del arreglo (apartado 6), si los mismos no están expuestos en la definición de ArrayNat?

Gracias! 

Saludos, Lía.

En respuesta a Lia Malvarez Busquets

Re: [Práctico 3] Ej: 8

de Carlos Luna -

Hola.

Efectivamente, son arreglos parametrizados en el largo (cantidad de elementos). En el caso de empty, es un ArrayNat 0, ya que no tiene elementos. Los arreglos no vacíos se construyen con add:

Parameter add : forall n:nat, nat -> ArrayNat n -> ArrayNat (n + 1).

Aquí el n:nat se usa para el tamaño del arreglo y el elemento que se agrega es el nat que marqué en negrita. Por ejemplo: (add 0 8 empty) es un arreglo que tendría solo el elemento 8 y tiene tamaño 1 (es de tipo ArrayNat 1); podría leerse/interpretarse como: "se agrega el 8 a un arreglo vacío (de tamaño 0) de naturales".   

Para generalizar el tipo de los elementos la idea es abstraer su tipo (con una variable de tipo Set). Por ejemplo en el add:

Parameter add' : forall (X : Set) (n : nat), X -> Array X n -> Array X (S n).

Saludos, Carlos