I'm looking for a type inference algorithm for a language I'm developing, but I couldn't find one that suits my needs because they usually are either:

In particular my type system is (simplifying) (I'm using Haskellish syntax but this is language agnostic):

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


And I've got an operator * which has got quite some overloads:

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

And I want to infer possible types for

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


The first is Int, the second Matrix Int.

Example (that doesn't work):

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

• This doesn't appear to meet the criteria for CS Theory Stack Exchange, but it does look like you're looking for a more mathematical or theoretical answer. I think that Computer Science may be appropriate for this. Since you requested a move to get better answers, I'll send it to where it is likely to be well-received. – Thomas Owens Apr 20 '14 at 21:00

I would suggest looking at Geoffrey Seward Smith's dissertation

As you probably already know, the way the common type inference algorithms work is that they traverse the syntax tree and for every subexpression they generate a type constraint. Then, they take this constraints, assume conjunction between them, and solve them (typically looking for a most general solution).

When you also have overloading, when analyzing an overloaded operator you generate several type constraints, instead of one, and assume disjunction between them, if the overloading is bounded. Because you are essentially saying that the operator can have either this, or this, or that type." If it is unbounded, one needs to resort to universal quantification, just as with polymorphic types, but with additional constraints that constrain the actual overloading types. The paper I reference covers these topics in more depth.

• Thank you very much, this is the answer I was looking for – miniBill Jun 10 '16 at 7:11

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


You're done! Well, except that you need defaulting. If your language allows defaulting the Times class to Int (and then Double), then your examples will work exactly as stated. The other way to fix it, of course, is to not automatically promote Int to Double, or to only do it when immediately necessary, and to use Int literals as Int only (again, promoting only when immediately necessary); this solution will also work.

• Thank you very much! (although the number of extensions is over 9k) – miniBill Apr 19 '14 at 20:58
• Doesn't work ideone.com/s9rSi7 – miniBill Apr 21 '14 at 11:24
• it's not a defaulting problem: ideone.com/LrfEjX – miniBill Apr 23 '14 at 17:58
• Oh, sorry, I misunderstood you then. Well, I don't want defaulting (I think).. – miniBill Apr 23 '14 at 18:48
• Could you try to produce an example that compiles? – miniBill Apr 24 '14 at 20:29