Construtor inteligente para tupla em Idris

Question

Comecei a ler o Capítulo 6 de "Desenvolvimento orientado a tipo com Idris" e tentei escrever um construtor inteligente para um vetor 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

Como criar um construtor para um k arbitrário?

Answer 1

Basicamente ideia de @Matthias Berndt. Contando regressivamente as setas a serem adicionadas, enquanto torna a tupla final mais longa. Para isso, precisamos acessar o ajudante mais permissivo 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

Porém, observe que isso resultará em \v2 => \v1 => (v1, v2, ())e não \v2 => \v1 => (v2, v1, ())como o primeiro se encaixa na definição recursiva de TupleVect (S k) a = (a, TupleVect k a)melhor.

Answer 2

Não sei quase nada sobre Idris, exceto que é uma linguagem do tipo Haskell, com tipagem dependente. Mas acho esse problema intrigante, então tentei.

Obviamente, você precisa de uma solução recursiva aqui. Minha ideia é usar um parâmetro adicional fque acumula os val1.. val_nparâmetros que a função comeu até agora. Quando o caso base é alcançado, fé retornado.

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

tupleVect n a = tupleVectHelper n a ()

Não tenho ideia se isso funciona e ainda não descobri como escrever o tipo de tupleVectHelper, mas tentei fazer as substituições manualmente n = 3e parece funcionar no papel, embora a tupla resultante esteja invertida. Mas acho que isso não deve ser muito difícil de consertar.

Espero que isto ajude!