Dans le cadre des grammaires catégorielles abstraites (ACG) introduites par Ph. de Groote, on peut faire des traductions entre différentes structures linguistiques, par exemple syntaxiques et sémantiques. Initialement conçu sur la base du lambda-calcul linéaire utilisé en linguistique, l'expressivité se trouve limitée notamment en sémantique, où l'on souhaiterait utiliser plusieurs fois une même variable. L'idée est alors d'introduire de l'intuitionisme, et donc un lambda-calcul avec deux types de variables et deux types de flèches (intuitionnistes et linéaires). Il est alors naturel de se demander quel peut être le type principal de termes de ce calcul, et quelles sont ses propriétés. Une difficulté provient du fait que lors de la recherche du type principal, des flèches sous-spécifiées peuvent apparaître, qui peuvent indifféremment être remplacées par les flèches linéaires ou des flèches intuitionistes. Pour ne pas compliquer ce lambda-calcul, il serait agréable de trouver des fragments pour lesquels on pourrait donner une notion de type principal sans flèche sous-spécifiée. Dans le cas général nous verrons que c'est impossible, mais que pour deux cas, le cas eta-long et le cas linéaire, nous avons un résultat.