Type system for higher kinded types, with inference

Is it possible to construct a type system that supports inference of higher kinded types in MPS? Has this been attempted before?

Haskell is a language which supports this.

For example:

fmap has type (Functor f) => (a -> b) -> f a -> f b
(+1) has type Int -> Int
(Just 5) has type Maybe Int
Maybe is a Functor


Therefore, in

fmap (+1) (Just 5)


It must be the case that

fmap has type (Int -> Int) -> Maybe Int -> Maybe Int


In most languages with generics you can specify something such as:

class List<T> {
   T value;
   List<T> next;
}


But you cannot declare something such as:

interface Functor<F> {
   function fmap<A,B>(f: A -> B, x: F<A>): F<B>;
}


Due to an error that is along the lines of "Cannot apply generic type 'F' to generic type 'A'; Cannot apply generic type 'F' to generic type 'B'" or "Generic types cannot be applied to generic types" or something like that.

From the tutorials I have seen, MPS appears closely related to the design of Java. I fear that down the road, after having invested a lot of time in learning MPS, that I will find deal breaking limitations in what kind of languages I am allowed to implement. Is this a good time to jump aboard with MPS?

Please sign in to leave a comment.