title: Is it possible to support higher-kinded types in Standard ML?
body: <p>I have read in <a href="https://stackoverflow.com/questions/1986374/higher-order-type-constructors-and-functors-in-ocaml">this post</a> that ML dialects do not allow type variables of non-ground kind. E.g. the last statement is not representable:</p>
  
  <pre class="lang-hs prettyprint-override"><code>-- Haskell code
  type Ground        = Int    
  type FirstOrder  a = Maybe a
  type SecondOrder c = c Int   -- ML do not allow :c
  </code></pre>
  
  <p>OCaml has support of higher-kinded only at the level of modules. There are some explanations (<a href="https://www.cl.cam.ac.uk/~jdy22/papers/lightweight-higher-kinded-polymorphism.pdf#page=2" rel="nofollow noreferrer">here</a> and author's comment <a href="https://discuss.ocaml.org/t/higher-kinded-polymorphism/2192/5" rel="nofollow noreferrer">here</a>) about which features of OCaml clash with higher-kinded types opportunity.</p>
  
  <p>If I understood it correctly, the main problem is in the following facts: </p>
  
  <ul>
  <li>OCaml does not follow a "freshness" restriction for type definitions: construct <code>type</code> can define both an alias (an the type will remain the same) and a new fresh type</li>
  <li>type alias definition can be hidden</li>
  </ul>
  
  <p>AFAIK, Standard ML has different constructs for type definition and aliases: <code>type</code> for aliases and <code>datatype</code> for new fresh types introduction.</p>
  
  <p>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?</p>
  
  <p>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.</p>