Concaténation de deux vecteurs - pourquoi les longueurs ne sont-elles pas traitées comme commutatives?

Question

Je suis jouer avec Idris et je suis tombé sur quelque chose qui me confond un peu:

Les contrôles de type:

conc : Vect n a -> Vect m a -> Vect (n+m) a 
conc [] ys = ys 
conc (x :: xs) ys = x :: (conc xs ys) 

mais cela ne veut pas:

conc : Vect n a -> Vect m a -> Vect (m+n) a 
conc [] ys = ys 
conc (x :: xs) ys = x :: (conc xs ys) 

avec l'erreur suivante:

When checking right hand side of conc with expected type 
     Vect (m + 0) a 

Type mismatch between 
     Vect m a (Type of ys) 
and 
     Vect (plus m 0) a (Expected type) 

Specifically: 
     Type mismatch between 
       m 
     and 
       plus m 0 

Equivalemment xs ++ y s vérifie le type mais ys ++ xs ne correspond pas à la définition du type de longueur n + m.

Cela me surprend un peu que l'addition est commutative. Y a-t-il quelque chose que je puisse faire (peut-être avec des contraintes?) À la signature de la fonction pour obtenir à la fois les expressions xs ++ ys et ys ++ xs.

Answer 1

Ceci est un sujet commun de confusion pour les débutants dans Idris. Le problème dans ce cas en deuxième version conc:

conc : Vect n a -> Vect m a -> Vect (m+n) a 
conc [] ys = ys 

Idris ne peut pas appliquer plus commutativity parce que Nat, plus commutativity est un théorème du point de vue du compilateur. Voici son type:

Idris> :t plusCommutative 
plusCommutative : (left : Nat) -> (right : Nat) -> left + right = right + left 

Il sommes pas de règles générales pour vous dire que le théorème de choisir et d'appliquer. Bien sûr, certaines heuristiques peuvent être faites pour des cas simples, comme Nat commutativité. Mais cela peut aussi rendre difficile de comprendre certains autres cas.

L'autre chose que vous devez considérer est la définition de plus:

Idris> :printdef plus 
plus : Nat -> Nat -> Nat 
plus 0 right = right 
plus (S left) right = S (plus left right) 

Fonction plus définie de telle manière qui est fait sur son modèle correspondant premier argument. Idris effectivement peut effectuer ce type de correspondance dans les types. Ainsi, en première version, où

conc : Vect n a -> Vect m a -> Vect (n+m) a 
conc [] ys = ys 

vous avez (0 + m) type et Idris peut remplacer plus 0 m avec m et tout typable. plus m 0 fonctionnerait si vous définissiez + opérateur par correspondance de modèle sur le second argument. Par exemple, cette compile:

infixl 4 +. 
(+.) : Nat -> Nat -> Nat 
n +. Z = n 
n +. (S m) = S (n +. m) 

conc : Vect n a -> Vect m a -> Vect (m +. n) a 
conc [] ys = ys 
conc (x :: xs) ys = x :: (conc xs ys) 

Mais il est évident que l'écriture nouvel opérateur pour tous les cas, vous avez besoin est horrible. Donc, pour faire votre deuxième version compilable vous devez utiliser la syntaxe rewrite ... in dans Idris.Vous avez besoin théorèmes suivants:

Idris> :t plusZeroRightNeutral 
plusZeroRightNeutral : (left : Nat) -> left + 0 = left 
Idris> :t plusSuccRightSucc 
plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + S right 
Idris> :t sym 
sym : (left = right) -> right = left 

Et voici la version qui compile:

conc : Vect n a -> Vect m a -> Vect (m + n) a 
conc   {m} []  ys = rewrite plusZeroRightNeutral m  in ys 
conc {n=S k} {m} (x :: xs) ys = rewrite (sym $ plusSuccRightSucc m k) in x :: (conc xs ys) 

Je ne suis pas ici pour expliquer comment rewriting et la démonstration de théorèmes fonctionne ici. C'est un sujet d'une autre question si vous ne comprenez pas quelque chose. Mais vous pouvez lire à ce sujet dans le tutoriel (ou attendre la sortie de The Book :).