Inferencia de tipo + sobrecarga

Estoy buscando un algoritmo de inferencia de tipos para un lenguaje que estoy desarrollando, pero no pude encontrar uno que se adapte a mis necesidades porque generalmente son:

• à la Haskell, con polimorfismo pero sin sobrecarga ad-hoc
• à la C ++ (auto) en el que tiene una sobrecarga ad-hoc pero las funciones son monomórficas

En particular, mi sistema de tipos es (simplificador) (estoy usando la sintaxis de Haskellish pero esto es independiente del lenguaje):

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

Y tengo un operador * que tiene algunas sobrecargas:

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 ...

Y quiero inferir posibles tipos para

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

El primero es Int, el segundo Matrix Int.

Ejemplo (que no funciona):

{-# 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

Sugeriría mirar la disertación de Geoffrey Seward Smith

Como probablemente ya sepa, la forma en que funcionan los algoritmos de inferencia de tipos comunes es que atraviesan el árbol de sintaxis y para cada subexpresión generan una restricción de tipo. Luego, toman estas restricciones, asumen la conjunción entre ellas y las resuelven (generalmente buscando la solución más general).

Cuando también tiene sobrecarga, al analizar un operador sobrecargado, genera varias restricciones de tipo, en lugar de una, y asume una disyunción entre ellas, si la sobrecarga está limitada. Debido a que esencialmente está diciendo que el operador puede tener `` esto, o esto, o ese tipo ''. Si no tiene límites, uno debe recurrir a la cuantificación universal, al igual que con los tipos polimórficos, pero con restricciones adicionales que limitan la realidad tipos de sobrecarga El documento al que me refiero cubre estos temas con más profundidad.

Por extraño que parezca, sí Haskell es perfectamente casi capaz de tu ejemplo; Hindley-Milner está totalmente bien con la sobrecarga, siempre que esté bien delimitado:

{-# 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

Ya terminaste! Bueno, excepto que necesitas incumplir. Si su idioma permite el valor predeterminado de la Timesclase Int(y luego Double), sus ejemplos funcionarán exactamente como se indica. La otra manera de solucionarlo, por supuesto, es la de no promover de forma automática Inta Double, o sólo lo hacen cuando inmediatamente necesaria, y para uso Intliterales como Intúnica (una vez más, la promoción sólo cuando sea necesario de inmediato); Esta solución también funcionará.