Type Idris découlant d'une opération arithmétique

Dans le code suivantType Idris découlant d'une opération arithmétique

Idris> :t \x => x + x 
\x => x + x : Integer -> Integer

Idris dérive d'un type entier pour une variable x où je pense qu'il devrait tirer une limitation de l'interface comme dans Haskell:

Haskell> :t (\x y -> x + y) 
(\x y -> x + y) :: Num a => a -> a -> a

Alors il ne se comporte même pas comme un entier, acceptant un type double:

Idris> (\x => x + x) 2.0 
4.0 : Double

Peut Quelqu'un me l'explique?

Source

2017-08-13 Ivan Kleshnin

L'inférence de type «Idris» n'est pas aussi mature que dans Haskell. Avec les types dépendants, votre inférence de type ne peut pas être aussi bonne. Probablement quelque chose de similaire à la restriction de monomorphisme se produit ici. Pour trouver une meilleure explication de ce comportement, vous devriez probablement ouvrir un bug dans le dépôt 'idris-dev': https://github.com/idris-lang/Idris-dev/issues – Shersh

Les types dépendants de @Shersh n'impliquent aucune limitation sur l'inférence de type pour les programmes non dépendants. En outre, ce cas concerne la généralisation plutôt que l'inférence, et Idris n'a pas de généralisation par conception, pas à cause d'une raison fondamentale. –

@ András Kovács pourriez-vous me diriger vers un contenu sur ce sujet "Idris n'a pas de généralisation par la conception"? –

Je pense qu'en général on peut dire que l'inspection de l'inférence de type dans la REPL d'idris est une mauvaise idée. Le code REPL et le code existant dans les fichiers Idris se comportent différemment.

Votre fonction souhaitée serait écrit:

addy: Num a => a -> a -> a 
addy x y = x + y

et aurait un type similaire à celui que vous attendez de Haskell. L'inférence de type dans Idris est en général très faible (car elle ne peut pas être décidée pour les systèmes de type typés de manière dépendante).

Source

2017-08-14 09:24:46 Markus

Type Idris découlant d'une opération arithmétique

Répondre

Questions connexes