I'm creating a semantic analyzer with type inference. For the basics I've got a type variable and a type construct with name and a list of types.

I want to support overloading and I know that Haskell uses something called type-classes. So if I understand correctly, when I call an overloaded function 'foo', I give multiple constraints for the parameters, so they have to match at least for one of them. For example:

// These are the 'instances' of a type-class
int operator+(int a, int b);
float operator+(float a, float b);

Then I call the operator:

var a, b;  // Can be any type
var c = a + b;

Then I can give (a, b) the constraint that it is either (int, int) or (float, float).

The extra unification steps would be type variable with type-class, type construct with type-class and type-class with type-class. In the first case, I guess it's just a simple substitution (from type variable to the type-class). What about the second case? I need to check if I'm able to unify with any of the instances. If there's none, it's an error (no such overload for function). If there's one, I've got an instance. But what if I have many matches? And the last case? I have no idea for that one (type-class with type-class).

If my assumptions are correct, what is a good data structure to do this? Do I just store constraints for both type variable and type construct and check those at unification?

Or am I approaching this badly and type-classes should not be part of the types and be constraints instead?

Edit: I didn't explain what I meant by type constructs. I mean types that have a name and one or more sub-types. For example an integer type has the name int and has no sub-types. A list could have the name vector like in c++ and a sub-type with the type of it's elements. A tuple could have many - varying amount of - sub-types, like: tuple<int, bool, string>.

  • 1
    $\begingroup$ Responding to your last question, type classes are a sort of constraint on type variables (in the sense of parametric polymorphism i.e. Java/C# "generics"), though they are certainly still part of an expression's type. You seem pretty unfamiliar with type classes and to be guessing at how they work and are used. I'd recommend getting some familiarity with type classes by using Haskell a bit, and also reading the literature on inferring/checking types in the presence of type classes. Your terminology, particularly "type construct", is idiosyncratic which makes it hard to be sure what you mean. $\endgroup$ May 29, 2017 at 10:11
  • $\begingroup$ @DerekElkins Sorry, it was a stupid mistake, I have explained what I meant by type constructs. I have downloaded GHC to play around with Haskell's type system and I'm getting the hang of it, the command :t is pretty useful there when experimenting. Still, I'm trying to look at it from an implementation perspective. $\endgroup$ May 29, 2017 at 11:19


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.