Constructeur intelligent pour tuple dans Idris

Question

J'ai commencé à lire le chapitre 6 de "Développement piloté par type avec Idris" et j'ai essayé d'écrire un constructeur intelligent pour un vecteur tuplé.

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

Comment créer un constructeur pour un k arbitraire?

Answer 1

Fondamentalement, l'idée de @Matthias Berndt. Compte à rebours des flèches à ajouter, tout en allongeant le tuple final. Pour cela, nous devons accéder à l'aide la plus permissive 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

Cependant, notez que cela se traduira par \v2 => \v1 => (v1, v2, ())et non \v2 => \v1 => (v2, v1, ())comme le premier correspond à la définition récursive de TupleVect (S k) a = (a, TupleVect k a)mieux.

Answer 2

Je ne sais presque rien d'Idris, sauf que c'est un langage de type Haskell typé de manière dépendante. Mais je trouve ce problème intriguant, alors je l'ai essayé.

Clairement, vous avez besoin d'une solution récursive ici. Mon idée est d'utiliser un paramètre supplémentaire fqui accumule les paramètres val1.. val_nque la fonction a mangés jusqu'à présent. Lorsque le cas de base est atteint, fest renvoyé.

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

tupleVect n a = tupleVectHelper n a ()

Je n'ai aucune idée si cela fonctionne, et je n'ai pas encore compris comment écrire le type de tupleVectHelper, mais j'ai essayé de faire les substitutions manuellement pour n = 3et cela semble fonctionner sur papier, bien que le tuple résultant soit à l'envers. Mais je pense que cela ne devrait pas être trop difficile à résoudre.

J'espère que cela t'aides!