Search code examples
smllanguage-designhigher-kinded-types

Is it possible to support higher-kinded types in Standard ML?

I have read in this post that ML dialects do not allow type variables of non-ground kind. E.g. the last statement is not representable:

-- Haskell code
type Ground        = Int    
type FirstOrder  a = Maybe a
type SecondOrder c = c Int   -- ML do not allow :c

OCaml has support of higher-kinded only at the level of modules. There are some explanations (here and author's comment here) about which features of OCaml clash with higher-kinded types opportunity.

If I understood it correctly, the main problem is in the following facts:

  • OCaml does not follow a "freshness" restriction for type definitions: construct type can define both an alias (an the type will remain the same) and a new fresh type
  • type alias definition can be hidden

AFAIK, Standard ML has different constructs for type definition and aliases: type for aliases and datatype for new fresh types introduction.

Unfortunatelly, I do not know SML well enough -- is it possible to export type aliases with its definition hidden? And can someone please show me if there are any other SML features that still do not go well with an opportunity of higher-kinded types?

Probably there will be some problems with functors -- Could one be so kind to show a code example of it? I've heard several times about such cases but still have not found a complete example of it.

Solution

  • Yes, SML can express the equivalent of higher-kinded types through functors, and can also make them abstract. Useless example:

    functor F (type 'a t) :> sig type 'a u end =
struct
    type 'a u = ('a t) t
end

    However, unlike OCaml, SML does not (officially) have higher-order functors, so per the standard, you can only express second-order type constructors this way.

    FWIW, OCaml may use the same keyword for type aliases and generative types (type vs datatype in SML), but they are still distinguished syntactically, by their right-hand side. So that's no real difference to SML.In both languages, an abstract occurring in a signature can be implemented as either a type alias or a generative type. So the problem for type inference that Leo is alluding to exists equally in both. Haskell can get away without that problem because it does not have the same expressiveness regarding type abstraction (i.e., no "sealing" operator for modules).