Inférence de type + surcharge

9

Je suis à la recherche d'un algorithme d'inférence de type pour un langage que je développe, mais je n'ai pas pu trouver celui qui correspond à mes besoins car ils sont généralement soit:

  • à la Haskell, avec polymorphisme mais sans surcharge ad hoc
  • à la C ++ (auto) dans laquelle vous avez une surcharge ad-hoc mais les fonctions sont monomorphes

En particulier, mon système de type est (simplifiant) (j'utilise la syntaxe Haskellish mais c'est indépendant du langage):

data Type = Int | Double | Matrix Type | Function Type Type

Et j'ai un opérateur * qui a pas mal de surcharges:

Int -> Int -> Int
(Function Int Int) -> Int -> Int
Int -> (Function Int Int) -> (Function Int Int)
(Function Int Int) -> (Function Int Int) -> (Function Int Int)
Int -> Matrix Int -> Matrix Int
Matrix Int -> Matrix Int -> Matrix Int
(Function (Matrix Int) (Matrix Int)) -> Matrix Int -> Matrix Int

Etc...

Et je veux déduire les types possibles pour

(2*(x => 2*x))*6
(2*(x => 2*x))*{{1,2},{3,4}}

Le premier est Int, le second Matrix Int.

Exemple (cela ne fonctionne pas):

{-# LANGUAGE OverlappingInstances, MultiParamTypeClasses,
  FunctionalDependencies, FlexibleContexts,
  FlexibleInstances, UndecidableInstances #-}

import qualified Prelude
import Prelude hiding ((+), (*))
import qualified Prelude

newtype WInt = WInt { unwrap :: Int }

liftW f a b = WInt $ f (unwrap a) (unwrap b)

class Times a b c | a b -> c where
(*) :: a -> b -> c

instance Times WInt WInt WInt where
(*) = liftW (Prelude.*)

instance (Times a b c) => Times a (r -> b) (r -> c) where
x * g = \v -> x * g v

instance Times (a -> b) a b where
f * y = f y

two = WInt 2
six = WInt 6

test :: WInt
test = (two*(\x -> two*x))*six

main = undefined
miniBill
la source
3
Cela ne semble pas répondre aux critères de CS Theory Stack Exchange, mais il semble que vous cherchiez une réponse plus mathématique ou théorique. Je pense que l'informatique peut être appropriée pour cela. Puisque vous avez demandé un coup pour obtenir de meilleures réponses, je vais l'envoyer là où il est susceptible d'être bien reçu.
Thomas Owens du

Réponses:

9

Je suggère de regarder la thèse de Geoffrey Seward Smith

Comme vous le savez probablement déjà, la façon dont les algorithmes d'inférence de type courants fonctionnent est qu'ils traversent l'arbre de syntaxe et pour chaque sous-expression, ils génèrent une contrainte de type. Ensuite, ils prennent ces contraintes, assument la conjonction entre elles et les résolvent (généralement à la recherche d'une solution la plus générale).

Lorsque vous avez également une surcharge, lors de l'analyse d'un opérateur surchargé, vous générez plusieurs contraintes de type, au lieu d'une, et supposez une disjonction entre elles, si la surcharge est limitée. Parce que vous dites essentiellement que l’opérateur peut avoir «soit ceci, soit ceci, soit ce type». types de surcharge. Le document que je référence couvre ces sujets de manière plus approfondie.

bellpeace
la source
Merci beaucoup, c'est la réponse que je cherchais
miniBill
7

Curieusement, Haskell lui - même est parfaitement presque capable de votre exemple; Hindley-Milner est très bien avec la surcharge, tant qu'elle est bien délimitée:

{-# LANGUAGE OverlappingInstances, MultiParamTypeClasses,
             FunctionalDependencies, FlexibleContexts,
             FlexibleInstances #-}
import Prelude hiding ((*))

class Times a b c | a b -> c where
    (*) :: a -> b -> c

instance Times Int Int Int where
    (*) = (Prelude.*)

instance Times Double Double Double where
    (*) = (Prelude.*)

instance (Times a b c) => Times (r -> a) (r -> b) (r -> c) where
    f * g = \v -> f v * g v

instance (Times a b c) => Times a (r -> b) (r -> c) where
    x * g = \v -> x * g v

instance (Times a b c) => Times (r -> a) b (r -> c) where
    f * y = \v -> f v * y

type Matrix a = (Int, Int) -> a

Vous avez terminé! Eh bien, sauf que vous avez besoin de défaut. Si votre langue autorise par défaut la Timesclasse à Int(puis Double), vos exemples fonctionneront exactement comme indiqué. L'autre façon de le fixer, bien sûr, est de ne pas promouvoir automatiquement Intà Double, ou ne le faire quand immédiatement nécessaire, et d'utiliser Intlittéraux comme Intseule (encore une fois, la promotion uniquement lorsque immédiatement nécessaire); cette solution fonctionnera également.

Flamme de Ptharien
la source
2
Merci beaucoup! (bien que le nombre d'extensions soit supérieur à 9k)
miniBill
1
Ne fonctionne pas ideone.com/s9rSi7
miniBill
1
ce n'est pas un problème par défaut: ideone.com/LrfEjX
miniBill
1
Oh, désolé, je vous ai alors mal compris. Eh bien, je ne veux pas faire défaut (je pense) ..
miniBill
2
Pourriez-vous essayer de produire un exemple qui compile?
miniBill