NDLI: 1ML – core and modules united (F-ing first-class modules)

Please wait, while we are loading the content...

Program synthesis: opportunities for the next decade

Functional pearl: a SQL to C compiler in 500 lines of code

1ML – core and modules united (F-ing first-class modules)

Applicative bidirectional programming with lenses

Noninterference for free

Denotational cost semantics for functional languages with inductive types

Functional programming and hardware design: still interesting after all these years

Pilsner: a compositionally verified compiler for a higher-order imperative language

Generating performance portable code using rewrite rules: from high-level functional expressions to high-performance OpenCL code

Which simple types have a unique inhabitant?

Functional pearl: two can keep a secret, if one of them uses Haskell

Practical principled FRP: forget the past, change the future, FRPNow!

RRB vector: a practical general purpose immutable sequence

Blame assignment for higher-order contracts with intersection and union

Practical SMT-based type error localization

An optimizing compiler for a purely functional web-application language

Bounded refinement types

Hygienic resugaring of compositional desugaring

Algebras and coalgebras in the light affine Lambda calculus

Analysing the complexity of functional programs: higher-order meets first-order

A unification algorithm for Coq featuring universe polymorphism and overloading

Adaptive lock-free maps: purely-functional to scalable

Elaborating evaluation-order polymorphism

HLIO: mixing static and dynamic typing for information-flow control in Haskell

Certified symbolic management of financial multi-party contracts

Functional pearl: a smart view on datatypes

Expressing contract monitors as patterns of communication

GADTs meet their match: pattern-matching warnings that account for GADTs, guards, and laziness

Pycket: a tracing JIT for a functional language

XQuery and static typing: tackling the problem of backward axes

Structures for structural recursion

Foundational extensible corecursion: a proof assistant perspective

Partial aborts for transactions via first-class continuations

Automatic refunctionalization to a language with copattern matching: with applications to the expression problem

A fast compiler for NetKAT

Efficient communication and collection with compact normal forms

Learning refinement types

1ML – core and modules united (F-ing first-class modules)

Content Provider	ACM Digital Library
Author	Rossberg, Andreas
Abstract	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. .
Starting Page	35
Ending Page	47
Page Count	13
File Format	PDF
ISBN	9781450336697
DOI	10.1145/2784731.2784738
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2015-08-29
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Elaboration Ml modules First-class modules Type systems System f Abstract data types Existential types
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

1ML – core and modules united (F-ing first-class modules)

F-ing modules

1ML – Core and Modules United (F-ing First-class Modules)

1ML – Core and Modules United (F-ing First-class Modules)

1ml — core and modules as one or: f-ing first-class modules.

Modeling abstract types in modules with open existential types

Programming with first-class modules in a core language with subtyping, singleton kinds and open existential types

Mixin' up the ML module system

Mixin’ Up the ML Module System

1ML – core and modules united (F-ing first-class modules)

Similar Documents

1ML – core and modules united (F-ing first-class modules)

F-ing modules

1ML – Core and Modules United (F-ing First-class Modules)

1ML – Core and Modules United (F-ing First-class Modules)

1ml — core and modules as one or: f-ing first-class modules.

Modeling abstract types in modules with open existential types

Programming with first-class modules in a core language with subtyping, singleton kinds and open existential types

Mixin' up the ML module system

Mixin’ Up the ML Module System

1ML – core and modules united (F-ing first-class modules)