Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

SML modules are a classic example of a "shadow language" ( https://gbracha.blogspot.com/2014/09/a-domain-of-shadows.htm... ). I'd like to see an ML-like language where modules/interfaces are normal values, functors are just normal functions, etc.

Modeling such a system at the value level is easy enough, but having it run at compile-time introduces some tricky issues (especially around IO).



Andreas Rossberg's 1ML is (was?) an effort to unify the module syntax with that of functions and values (https://people.mpi-sws.org/~rossberg/papers/Rossberg%20-%201..., https://github.com/rossberg/1ml)

The module syntax is certainly clumsy in comparison to the rest of the language, and it's not just the syntax - everything about functor arguments is a bit murky.


Thanks for the link, it looks just like what I was after!

I've been reading through the paper and it looks really nice. It seems to rely on dependent records, which I assumed might be the case; but it claims the dependency is "benign" and elaborates-way when translated to System-F (I haven't reached that part yet); so it does seem to have found the right "trick" (i.e. a tractable subset of dependent types which enables modules, without losing too much inference or devolving into a game of prove-the-lemma).

Incidentally, it's also a nice use of "first class types" which isn't (fully) dependently-typed. It irks me when I read blog posts about e.g. Agda or Idris, which describe first-class types (i.e. no stratification, passing types in and out of functions, etc.) but call that "dependent types"; then don't mention the actual "dependent" part (type signatures which bind values to names, which can be referenced "later on" in the type).


Is ML used in industry? If so, what would be the scenarios/use cases?


> what would be the scenarios/use cases?

MLs are good at representing and manipulating complicated data with intricate invariants (e.g. using algebraic data types for representions, pattern-matching for traversing/manipulating data, abstract/existential types for encapsulation and enforcing interfaces, etc.). In practice this makes it good for handling other languages (after all, "ML" stands for "meta language").

Its original purpose was manipulating mathematical proofs/expressions, and it's still popular for that, e.g. Isabelle's core is written in PolyML, Coq is written in Ocaml, and I think some others like the various HOLs use it too; note that these see a little use in industry for verification (although some famous verification examples, like AMD's FPU verification, used ACL2 which is based on Lisp rather than ML).

It's also good for manipulating Web languages like HTML and Javascript, which has spawned a few compile-to-Web languages which are ML-like or implemented in ML, e.g. http://opalang.org and http://www.impredicative.com/ur . This might also be why Facebook made/use Reason ( https://reasonml.github.io ), which AFAIK is an alternative syntax for Ocaml.

Jane Street seem to be heavy users of Ocaml, since they sponsor a lot of work on the compiler and infrastructure.


The wiki page for SML claims it's used by chip manufacturers like ARM, but no citation.

However, languages like Ocaml and F# are direct descendants of ML, and those languages see wider modern adoption. In this sense ML is kind of equivalent to C, and something like Ocaml is kind of equivalent to C++. Haskell is also in the ML family but its laziness and emphasis on purity keeps it a bit separate from its cousins.

In general, FP sees adoption where correctness is of overriding importance -- e.g., Jane Street's use of Ocaml.


ML is a general-purpose programming language, and as such its use case cannot be narrowly specified. (They say it's good for writing compilers, but I wouldn't latch on that.)


He asked if it was used in industry. This can be answered by looking at job postings or TIOBE.


OCaml has first-class modules & functors (functions on modules). I can write something like:

  let f (type t) some_arg (module M : Stringable with type t = t) = M.to_string some_arg
This will have the type signature

  val f : 'a -> (module Stringable with type t = 'a) -> string
In this case the module type Stringable looks like:

  module type Stringable = sig
    type t
    val to_string : t -> string
Functors are just module types so can be used in the same way. Module types fit in as normal values, you don't have to pattern match on them. This works:

  let id x = x
  
  id (module Int)


Interesing; I've not used Ocaml much (mostly just reading, e.g. the Coq source), so I'm more familiar with StandardML's more verbose separation.


Scala is interesting in this sense; I'd consider it to be an ML-like language. It attempts to unify object systems and module systems, and they are fairly first class in Scala. Modules (objects) can be used as normal values; you can encode functors as functions or classes as needed; signatures (traits) are usable as values to some degree, too.

>Furthermore, path-dependent types allow Scala to unify modules and objects, so that the same language constructs can be used to specify the overall structure of a program as well as its implementation details. The unification of the module and term languages is witnessed by the following comparison with the ML module system: Scala objects correspond to ML modules, classes to functors, and interfaces to signatures [Odersky and Zenger 2005].

https://arxiv.org/pdf/1904.07298.pdf




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: