Constructor inteligente para tuplas en Idris

Question

Comencé a leer el Capítulo 6 de "Desarrollo basado en tipos con Idris" e intenté escribir un constructor inteligente para un vector tuplado.

TupleVect : Nat -> Type -> Type
TupleVect Z _ = ()
TupleVect (S k) a = (a, TupleVect k a)

someValue : TupleVect 4 Nat
someValue = (1,2,3,4,())

TupleVectConstructorType : Nat -> Type -> Type
TupleVectConstructorType n typ = helper n
  where
    helper : Nat -> Type
    helper Z = TupleVect n typ
    helper (S k) = typ -> helper k

tupleVect : (n : Nat) -> (a : Type) -> TupleVectConstructorType n a
tupleVect Z a = ()
tupleVect (S Z) a = \val => (val, ())
tupleVect (S (S Z)) a = \val2 => \val1 => (val2, val1, ())
-- ??? how to create tupleVect (S k) a

¿Cómo crear un constructor para una k arbitraria?

Answer 1

Básicamente la idea de @Matthias Berndt. Contando las flechas que se agregarán, mientras alarga la tupla final. Para ello, necesitamos acceder al ayudante más permisivo de TupleVectType.

TupleVectType' : Nat -> Nat -> Type -> Type
TupleVectType' Z n a = TupleVect n a
TupleVectType' (S k) n a = a -> TupleVectType' k (S n) a

TupleVectType : Nat -> Type -> Type
TupleVectType n = TupleVectType' n Z

tupleVect : (n : Nat) -> (a : Type) -> TupleVectType n a
tupleVect n a = helper n Z a ()
    where
        helper : (k, n : Nat) -> (a : Type) -> (acc : TupleVect n a)
            -> TupleVectType' k n a
        helper Z n a acc = acc
        helper (S k) n a acc = \x => helper k (S n) a (x, acc)

someValue2 : TupleVect 4 Nat
someValue2 = (tupleVect 4 Nat) 4 3 2 1

Aunque tenga en cuenta que esto dará como resultado \v2 => \v1 => (v1, v2, ())y no \v2 => \v1 => (v2, v1, ())como el primero se ajusta a la definición recursiva de TupleVect (S k) a = (a, TupleVect k a)mejor.

Answer 2

No sé casi nada sobre Idris, excepto que es un lenguaje de tipo Haskell de tipo dependiente. Pero encuentro este problema intrigante, así que lo intenté.

Claramente, necesita una solución recursiva aquí. Mi idea es usar un parámetro adicional fque acumule los val1.. val_nparámetros que la función ha comido hasta ahora. Cuando se alcanza el caso base, fse devuelve.

tupleVectHelper Z a f = f
tupleVectHelper (S n) a f = \val => tupleVectHelper n a (val, f)

tupleVect n a = tupleVectHelper n a ()

No tengo idea de si esto funciona, y aún no he descubierto cómo escribir el tipo de tupleVectHelper, pero intenté hacer las sustituciones manualmente n = 3y parece funcionar en papel, aunque la tupla resultante está al revés. Pero creo que eso no debería ser demasiado difícil de solucionar.

¡Espero que esto ayude!