[Solved]: Type inference + overloading

Problem Detail: 

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:

• à la Haskell, with polymorphism but no ad-hoc overloading
• à la C++ (auto) in which you have ad-hoc overloading but functions are monomorphic

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 

Asked By : miniBill

Answered By : bellpeace

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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/23963

 Ask a Question

 Download Related Notes/Documents