Вывод типа + перегрузка

Я ищу алгоритм вывода типов для разрабатываемого языка, но я не смог найти тот, который удовлетворял бы моим потребностям, потому что они обычно таковы:

• à la Haskell, с полиморфизмом, но без специальной перегрузки
• C ++ (авто), в котором у вас есть временная перегрузка, но функции мономорфны

В частности, моя система типов (упрощенная) (я использую синтаксис Haskellish, но это не зависит от языка):

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

И у меня есть оператор *, который имеет довольно много перегрузок:

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

Так далее...

И я хочу сделать вывод о возможных типах для

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

Первое Int, второе Matrix Int.

Пример (это не работает):

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

Я бы предложил посмотреть на диссертацию Джеффри Сьюарда Смита

Как вы, наверное, уже знаете, алгоритм работы вывода общего типа работает так, что они пересекают синтаксическое дерево и для каждого подвыражения генерируют ограничение типа. Затем они берут эти ограничения, предполагают связь между ними и решают их (обычно ищут наиболее общее решение).

Когда у вас также есть перегрузка, при анализе перегруженного оператора вы генерируете несколько ограничений типа, вместо одного, и допускаете разделение между ними, если перегрузка ограничена. Потому что вы, по сути, говорите, что оператор может иметь «или то, или это, или тот тип». Если он не ограничен, нужно прибегнуть к универсальному количественному определению, так же, как с полиморфными типами, но с дополнительными ограничениями, которые ограничивают действительный Перегрузка типов. В статье, на которую я ссылаюсь, эти темы рассматриваются более подробно.

Как ни странно, сам Haskell является совершенно почти способен ваш пример; Хиндли-Милнер вполне справляется с перегрузкой, если она хорошо ограничена:

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

Вы сделали! Ну разве что нужно дефолт. Если ваш язык позволяет установить по умолчанию Timesкласс Int(и затем Double), тогда ваши примеры будут работать точно так, как указано. Другой способ исправить это, конечно, не автоматически продвигать Intк Double, или только делать это , когда сразу же необходимо, и использование Intлитералов , как Intтолько (опять же , продвигая только тогда , когда сразу необходимо); это решение также будет работать.