Alexis, have you seen this?:
https://people.mpi-sws.org/~rossberg/1ml/
"ML is two languages in one: there is the core, with types and
expressions, and there are modules, with signatures, structures and
functors. Modules form a separate, higher-order functional language on
top of the core. There are both practical and technical reasons for this
stratification; yet, it creates substantial duplication in syntax and
semantics, and it reduces expressiveness. For example, selecting a
module cannot be made a dynamic decision. Language extensions allowing
modules to be packaged up as first-class values have been proposed and
implemented in different variations. However, they remedy expressiveness
only to some extent, are syntactically cumbersome, and do not alleviate
redundancy."
"We propose a redesign of ML in which modules are truly first-class
values, and core and module layer are unified into one language. In this
"1ML", functions, functors, and even type constructors are one and the
same construct; likewise, no distinction is made between structures,
records, or tuples. Or viewed the other way round, everything is just
("a mode of use of") modules. Yet, 1ML does not require dependent types,
and its type structure is expressible in terms of plain System Fω, in a
minor variation of our F-ing modules approach. We introduce both an
explicitly typed version of 1ML, and an extension with
Damas/Milner-style implicit quantification. Type inference for this
language is not complete, but, we argue, not substantially worse than
for Standard ML.
"An alternative view is that 1ML is a user-friendly surface syntax for
System Fω that allows combining term and type abstraction in a more
compositional manner than the bare calculus."
--
Anthony Carrico
--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
