Inférence de type + surcharge

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

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.

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.