Wnioskowanie typu + przeciążenie

Szukam algorytmu wnioskowania typu dla języka, który rozwijam, ale nie mogłem znaleźć takiego, który odpowiada moim potrzebom, ponieważ zwykle są to:

• à la Haskell, z polimorfizmem, ale bez przeładowania ad hoc
• à la C ++ (auto), w którym występuje przeciążenie ad-hoc, ale funkcje są monomorficzne

W szczególności mój system typów (upraszcza) (używam składni Haskellisha, ale jest to zależne od języka):

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

I mam operatora *, który ma dość przeciążenia:

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

Itp...

I chcę wywnioskować możliwe typy dla

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

Pierwszy to Intdrugi Matrix Int.

Przykład (to nie działa):

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

Proponuję spojrzeć na rozprawę Geoffrey'a Sewarda Smitha

Jak zapewne już wiesz, sposób działania typowych algorytmów wnioskowania typu polega na tym, że przechodzą one przez drzewo składniowe i dla każdego podwyrażenia generują ograniczenie typu. Następnie biorą te ograniczenia, zakładają połączenie między nimi i rozwiązują je (zwykle szukając najbardziej ogólnego rozwiązania).

W przypadku przeciążenia, analizując przeciążonego operatora, generujesz kilka ograniczeń typu zamiast jednego i zakładasz rozłączenie między nimi, jeśli przeciążenie jest ograniczone. Ponieważ zasadniczo mówisz, że operator może mieć `` ten, ten lub ten, lub ten typ. '' Jeśli jest nieograniczony, należy zastosować uniwersalną kwantyfikację, podobnie jak w przypadku typów polimorficznych, ale z dodatkowymi ograniczeniami, które ograniczają rzeczywiste rodzaje przeciążenia. Dokument, który przytaczam, omawia te tematy bardziej szczegółowo.

Co dziwne, sama Haskell jest doskonale prawie zdolny swoim przykładzie; Hindley-Milner jest całkowicie w porządku z przeciążeniem, o ile jest dobrze ograniczony:

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

Jesteś skończony! Cóż, z wyjątkiem tego, że potrzebujesz domyślnego. Jeśli twój język pozwala na domyślną Timesklasę Int(a następnie Double), twoje przykłady będą działać dokładnie tak, jak podano. Innym sposobem, aby naprawić to, oczywiście, nie jest automatycznie promować Intsię Double, czy aby tylko zrobić to natychmiast, gdy to konieczne, i do użytku Intliterałów jako Intjedyny (ponownie, gdy tylko promowanie natychmiast konieczne); to rozwiązanie będzie również działać.