mlton-user — [MLton-user] User community discussion

[MLton-user] ICFP 2026: Call for Papers

['ICFP P. v. MLton-u. <mlt...@ml...>]

ICFP 2026 Call for Papers

Accepted papers to be invited for presentation at:


*The 31st ACM SIGPLAN International Conference on Functional Programming*August
23-29, 2026
Indianapolis, Indiana, USA
https://icfp26.sigplan.org
------------------------------

Submission Information

   - *Submission web site*: https://icfp26.hotcrp.com
   - *Submission Deadline*: 19 Feb 2026 (AoE)

Double-blind review

   - Reviews: 20 Apr 2026 (AoE)
   - Author Response: 20 Apr 2026 - 23 Apr 2026 (AoE)
   - Notification of Conditional Acceptance: 14 May 2026 (AoE)
   - Revision: 3 Jun 2026 (AoE)
   - Final Notification: 10 Jun 2026 (AoE)
   - Camera Ready: 1 Jul 2026 (AoE)

------------------------------

PACMPL issue ICFP 2026 seeks original papers on the art and science of
functional programming. Submissions are invited on all topics from
principles to practice, from foundations to features, and from abstraction
to application. The scope includes all languages that encourage functional
programming, including both purely applicative and imperative languages, as
well as languages with objects, concurrency, or parallelism. Topics of
interest include (but are not limited to):

   -

   Language Design: concurrency, parallelism, and distribution; modularity;
   components and composition; meta-programming; macros; pattern matching;
   type systems; type inference; dependent types; effect types; gradual types;
   refinement types; session types; interoperability; domain-specific
   languages; imperative programming; object-oriented programming; logic
   programming; probabilistic programming; reactive programming; generic
   programming; bidirectional programming; secure programming.
   -

   Implementation: abstract machines; virtual machines; interpretation;
   compilation; compile-time and run-time optimisation; garbage collection and
   memory management; runtime systems; multi-threading; exploiting parallel
   hardware; interfaces to foreign functions, services, components, or
   low-level machine resources.
   -

   Software-Development Techniques: algorithms and data structures; design
   patterns; specification; verification; validation; proof assistants;
   debugging; testing; tracing; profiling; build systems; program synthesis.
   -

   Analysis and Transformation: control flow; data flow; abstract
   interpretation; partial evaluation; program calculation.
   -

   Foundations: formal semantics; lambda calculus; program equivalence;
   rewriting; type theory; logic; category theory; computational effects;
   continuations; control; state; names and binding; program verification.
   -

   Applications: symbolic computing; formal-methods tools; systems
   programming; distributed systems and web programming; hardware design;
   databases; scientific and numerical computing; graphical user interfaces;
   graphics and multimedia; GPU programming; scripting; system administration;
   security.
   -

   Education: teaching introductory programming; mathematical proof;
   algebra.

Submissions will be evaluated according to their relevance, correctness,
significance, originality, and clarity. Each submission should explain its
contributions in both general and technical terms, clearly identifying what
has been accomplished, explaining why it is significant, and comparing it
with previous work. The technical content should be accessible to a broad
audience.

PACMPL issue ICFP 2026 also welcomes submissions in two separate categories
— Functional Pearls and Experience Reports — that must be marked as such
when submitted and that *need not* report original research results.
Detailed guidelines on both categories are given at the end of this call.

In an effort to achieve a balanced, diverse program, each author may be
listed as a (co)author on a maximum of four submissions. Authors who
require financial support to attend the conference can apply for PAC
funding (http://www.sigplan.org/PAC/).

The General Chair and PC Chair may not submit papers. PC members (other
than the PC Chair) may submit papers.

Please contact the Program Chair if you have questions or are concerned
about the appropriateness of a topic.
Double-blind Submissions
<https://icfp26.sigplan.org/track/icfp-2026-icfp-papers#double-bind-submissions>

ICFP 2026 will use a full double-blind reviewing process. This means that
identities of authors will not be made visible to reviewers until after
conditional-acceptance decisions have been made, and then only for the
conditionally-accepted papers. The use of full double-blind reviewing has
several consequences for authors.

   -

   Submissions: Authors must omit their names and institutions from their
   paper submissions. In addition, references to authors’ own prior work
   should be in the third person (e.g., not “We build on our previous work …”
   but rather “We build on the work of …”).
   -

   Supplementary material: Authors must fully anonymize any supplementary
   material (see below). Links to supplementary material on external websites
   are not permitted.
   -

   Author response: In responding to reviews, authors should not say
   anything that reveals their identity, since author identities will not be
   revealed to reviewers at that stage of the reviewing process.
   -

   Dissemination of work under submission: Authors are welcome to
   disseminate their ideas and post draft versions of their paper(s) on their
   personal website, institutional repository, or arXiv (reviewers will be
   asked to turn off arXiv notifications during the review period). But
   authors should not take steps that would almost certainly reveal their
   identities to members of the Program Committee, e.g., directly contacting
   PC members or publicizing the work on widely-visible social media or major
   mailing lists used by the community.

The purpose of the above restrictions is to help the Program Committee come
to a judgment about the paper without bias, not to make it impossible for
them to discover the authors’ identities if they were to try. In
particular, nothing should be done in the name of anonymity that weakens
the quality of the submission. However, there are occasionally cases where
adhering to the above restrictions is truly difficult or impossible for one
reason or another. In such cases, the authors should contact the Program
Chair to discuss the situation and how to handle it. The FAQ on
Double-Blind Reviewing (
https://popl24.sigplan.org/track/POPL-2024-popl-research-papers#FAQ-on-Double-Blind-Reviewing)
addresses many common scenarios and answers many common questions about
this topic. But there remain many grey areas and trade-offs. If you have
any doubts about how to interpret the double-blind rules or you encounter a
complex case that is not clearly covered by the FAQ, please contact the
Program Chair for guidance.
Preparation of submissions
<https://icfp26.sigplan.org/track/icfp-2026-icfp-papers#preparation-of-submissions>

The deadline for submissions is: *** Thursay, 19 Feb 2026 AoE *** (
https://www.timeanddate.com/time/zones/aoe). This deadline will be strictly
enforced.

   -

   Formatting: Submissions must be in PDF format, printable in black and
   white on US Letter sized paper and interpretable by common PDF tools. All
   submissions must adhere to the “ACM Small” template that is available (in
   both LaTeX and Word formats) from
   https://www.acm.org/publications/authors/submissions.

   Please download the latest version of the ACM style from
   https://www.acm.org/publications/authors/submissions, since the citation
   format has recently been changed.

   See also PACMPL’s Information and Guidelines for Authors at
   https://pacmpl.acm.org/authors.cfm.

   There is a limit of *25 pages* for a full paper or Functional Pearl and *12
   pages* for an Experience Report; in either case, the bibliography and an
   optional clearly marked appendix will not be counted against these limits.
   Submissions that exceed the page limits or, for other reasons, do not meet
   the requirements for formatting, will be desk rejected.
   -

   Submission: Submissions will be accepted at https://icfp26.hotcrp.com

   Improved versions of a paper may be submitted at any point before the
   submission deadline using the same web interface.
   -

   Author Response Period: Authors will have a 96-hour period, starting at
   00:00 (midnight) AoE on Monday, 20 April, 2026, to read reviews and respond
   to them.
   -

   Appendix and Supplementary Material: Authors have the option to include
   a clearly marked appendix and/or to attach supplementary material to a
   submission, on the understanding that reviewers may choose not to look at
   such an appendix or supplementary material. Supplementary material may be
   uploaded as a separate PDF document or tarball. Any supplementary material
   must be uploaded at submission time, not by providing a URL in the paper
   that points to an external repository. All supplementary material must be
   anonymised.
   -

   Authorship Policies: All submissions are expected to comply with the ACM
   Policies for Authorship that are detailed at
   https://www.acm.org/publications/authors/information-for-authors.
   -

   Republication Policies: Each submission must adhere to SIGPLAN’s
   republication policy, as explained on the web at
   http://www.sigplan.org/Resources/Policies/Republication.

Review Process
<https://icfp26.sigplan.org/track/icfp-2026-icfp-papers#review-process>

This section outlines the two-stage process with double-blind reviewing
that will be used to select papers for PACMPL issue ICFP 2026. Like last
year, ICFP 2026 will adapt a full double-blind reviewing process. More
information see below.

ICFP 2026 will have two Associate Chairs who will help the PC Chair monitor
reviews, solicit external expert reviews for submissions when there is not
enough expertise on the committee, and facilitate reviewer discussions.

ICFP 2026 will employ a two-stage review process. The first stage in the
review process will assess submitted papers using the criteria stated above
and will allow for feedback and input on initial reviews through the author
response period mentioned previously. As a result of the review process, a
set of papers will be conditionally accepted and all other papers will be
rejected. Authors will be notified of these decisions on 14 May, 2026.

Authors of conditionally accepted papers will be provided with committee
reviews along with a set of optional or mandatory revisions. By 3 June,
2026, the authors should provide a revised submission. The second and final
reviewing phase assesses whether the mandatory revisions have been
adequately addressed by the authors and thereby determines the final
accept/reject status of the paper. The intent and expectation is that the
mandatory revisions can feasibly be addressed within a couple of weeks.

The second submission should clearly identify how the mandatory revisions
were addressed. To that end, the second submission *must be accompanied by
a cover letter* mapping each mandatory revision request to specific parts
of the paper. The cover letter will facilitate a quick second review,
allowing for confirmation of final acceptance within two weeks. Conversely,
the absence of a cover letter will be grounds for the paper’s rejection.
Information for Authors of Accepted Papers
<https://icfp26.sigplan.org/track/icfp-2026-icfp-papers#information-for-authors-of-accepted-papers>

As a condition of acceptance, final versions of all papers must adhere to
the ACM Small format. The page limit for the final versions of papers will
be *increased by two pages* to help authors respond to reviewer comments
and mandatory revisions: 27 pages plus bibliography for a regular paper or
Functional Pearl, 14 pages plus bibliography for an Experience Report.

Authors of accepted submissions will be required to agree to one of the
three ACM licensing options, one of which is Creative Commons CC-BY
publication; this is the option recommended by the PACMPL editorial board.
A reasoned argument in favour of this option can be found in the article
Why CC-BY? published by OASPA, the Open Access Scholarly Publishers
Association. The other options are copyright transfer to ACM or retaining
copyright but granting ACM exclusive publication rights.

PACMPL is a Gold Open Access journal, and authors are encouraged to publish
their work under a CC-BY license. Gold Open Access guarantees permanent
free online access to the definitive version in the ACM Digital Library,
and the recommended CC-BY option also allows anyone to copy and distribute
the work with attribution. Gold Open Access has been made possible by
generous funding through ACM SIGPLAN, which will cover all open access
costs in the event authors cannot. Authors who can cover the costs may do
so by paying an Article Processing Charge (APC). PACMPL, SIGPLAN, and ACM
Headquarters are committed to exploring routes to making Gold Open Access
publication both affordable and sustainable.

ACM Author-Izer is a unique service that enables ACM authors to generate
and post links on either their home page or institutional repository for
visitors to download the definitive version of their articles from the ACM
Digital Library at no charge. Downloads through Author-Izer links are
captured in official ACM statistics, improving the accuracy of usage and
impact measurements. Consistently linking to the definitive version of an
ACM article should reduce user confusion over article versioning. After an
article has been published and assigned to the appropriate ACM Author
Profile pages, authors should visit
http://www.acm.org/publications/acm-author-izer-service to learn how to
create links for free downloads from the ACM DL.

The official publication date is the date the journal is made available in
the ACM Digital Library. The journal issue and associated papers will be
published no earlier than 1 August, 2026. The official publication date
affects the deadline for any patent filings related to published work.

Authors of each accepted submission are invited to attend and be available
for the presentation of that paper at the conference. The schedule for
presentations will be determined and shared with authors after the full
program has been selected.

ORCID: ORCID provides a persistent digital identifier (an ORCID iD) that
you own and control, and that distinguishes you from every other
researcher: https://orcid.org/. ACM now require an ORCID iD for every
author of a paper, not just the corresponding author. So, the author who is
filling out the permission form should make sure they have the ORCID iDs
for all of their coauthors before filling out the form. Any authors who do
not yet have an ORCID iD can go to https://orcid.org/register to have one
assigned.

By submitting your article to an ACM Publication, you are hereby
acknowledging that you and your co-authors are subject to all ACM
Publications Policies, including ACM’s new Publications Policy on Research
Involving Human Participants and Subjects. Alleged violations of this
policy or any ACM Publications Policy will be investigated by ACM and may
result in a full retraction of your paper, in addition to other potential
penalties, as per ACM Publications Policy.
Artifact Evaluation
<https://icfp26.sigplan.org/track/icfp-2026-icfp-papers#artifact-evaluation>

Authors of papers that are conditionally accepted in the first phase of the
review process will be encouraged (but not required) to submit supporting
materials for Artifact Evaluation. These items will then be reviewed by an
Artifact Evaluation Committee, separate from the paper Review Committee,
whose task is to assess how the artifacts support the work described in the
associated paper. Papers that go through the Artifact Evaluation process
successfully will receive a seal of approval printed on the papers
themselves. Authors of accepted papers will be encouraged to make the
supporting materials publicly available upon publication of the papers, for
example, by including them as “source materials” in the ACM Digital
Library. An additional seal will mark papers whose artifacts are made
available, as outlined in the ACM guidelines for artifact badging.

Participation in Artifact Evaluation is voluntary and *will not influence* the
final decision regarding paper acceptance.
Special categories of papers
<https://icfp26.sigplan.org/track/icfp-2026-icfp-papers#special-categories-of-papers>

In addition to research papers, PACMPL issue ICFP solicits two kinds of
papers that do not require original research contributions: Functional
Pearls, which are full papers, and Experience Reports, which are limited to
half the length of a full paper. Authors submitting such papers should
consider the following guidelines.
Functional Pearls
<https://icfp26.sigplan.org/track/icfp-2026-icfp-papers#functional-pearls>

A Functional Pearl is an elegant essay about something related to
functional programming. Examples include, but are not limited to:

   - a new and thought-provoking way of looking at an old idea;
      - an instructive example of program calculation or proof;
      - a nifty presentation of an old or new data structure;
      - an interesting application of functional programming techniques;
      - a novel use or exposition of functional programming in the
      classroom.

While pearls often demonstrate an idea through the development of a short
program, there is no requirement or expectation that they do so. Thus, they
encompass the notions of theoretical and educational pearls.

Functional Pearls are valued as highly and judged as rigorously as ordinary
papers, but using somewhat different criteria. In particular, a pearl is
not required to report original research, but, it should be concise,
instructive, and entertaining. A pearl is likely to be rejected if its
readers get bored, if the material gets too complicated, if too
much-specialised knowledge is needed, or if the writing is inelegant. The
key to writing a good pearl is polishing.

A submission that is intended to be treated as a pearl must be marked as
such on the submission web page and should contain the words “Functional
Pearl” somewhere in its title or subtitle. These steps will alert reviewers
to use the appropriate evaluation criteria. Pearls will be combined with
ordinary papers for the purpose of computing the conference’s acceptance
rate.
Experience Reports
<https://icfp26.sigplan.org/track/icfp-2026-icfp-papers#experience-reports>

The purpose of an Experience Report is to describe the experience of using
functional programming in practice, whether in industrial application, tool
development, programming education, or any other area.

Possible topics for an Experience Report include, but are not limited to:

   - insights gained from real-world projects using functional programming;
      - comparison of functional programming with conventional programming
      in the context of an industrial project or a university curriculum
      project-management, business, or legal issues encountered when using
      functional programming in a real-world project;
      - curricular issues encountered when using functional programming in
      education;
      - real-world constraints that created special challenges for an
      implementation of a functional language or for functional programming in
      general.

An Experience Report is distinguished from a normal PACMPL issue ICFP paper
by its title, by its length, and by the criteria used to evaluate it.

Both in the papers and in any citations, the title of each accepted
Experience Report must end with the words “(Experience Report)” in
parentheses. The acceptance rate for Experience Reports will be computed
and reported separately from the rate for ordinary papers.

Experience Report submissions can be at most 12 pages long, excluding
bibliography.

Each accepted Experience Report will be presented at the conference, but
depending on the number of Experience Reports and regular papers accepted,
authors of Experience Reports may be asked to give shorter talks.

Because the purpose of Experience Reports is to enable our community to
understand the application of functional programming, an acceptable
Experience Report need not add to the body of knowledge of the
functional-programming community by presenting novel results or
conclusions. It is sufficient if the report describes an illuminating
experience with functional programming, or provides evidence for a clear
thesis about the use of functional programming. The experience or thesis
must be relevant to ICFP, but it need not be novel.

The review committee will accept or reject Experience Reports based on
whether they judge the paper to illuminate some aspect of the use of
functional programming. Anecdotal evidence will be acceptable provided it
is well-argued and the author explains what efforts were made to gather as
much evidence as possible. Typically, papers that show how functional
programming was used are more convincing than papers that say only that
functional programming was used. It can be especially effective to present
comparisons of the situations before and after the experience described in
the paper, but other kinds of evidence would also make sense, depending on
context. Experience drawn from a single person’s experience may be
sufficient, but more weight will be given to evidence drawn from the
experience of groups of people.

An Experience Report should be short and to the point. For an industrial
project, it should make a claim about how well functional programming
worked and why; for a pedagogy paper, it might make a claim about the
suitability of a particular teaching style or educational exercise. Either
way, it should produce evidence to substantiate the claim. If functional
programming worked in this case in the same ways it has worked for others,
the paper need only summarise the results — the main part of the paper
should discuss how well it worked and in what context. Most readers will
not want to know all the details of the experience and its implementation,
but the paper should characterise it and its context well enough so that
readers can judge to what degree this experience is relevant to their own
circumstances. The paper should take care to highlight any unusual aspects;
specifics about the experience are more valuable than generalities about
functional programming.

If the paper not only describes experience but also presents new technical
results, or if the experience refutes cherished beliefs of the
functional-programming community, it may be better to submit it as a full
paper, which will be judged by the usual criteria of novelty, originality,
and relevance. The Program Chair will be happy to advise on any concerns
about which category to submit to.
About PACMPL
<https://icfp26.sigplan.org/track/icfp-2026-icfp-papers#about-pacmpl>

Proceedings of the ACM on Programming Languages (PACMPL
https://pacmpl.acm.org/) is a Gold Open Access journal publishing research
on all aspects of programming languages, from design to implementation and
from mathematical formalisms to empirical studies. Each issue of the
journal is devoted to a particular subject area within programming
languages and will be announced through publicised Calls for Papers, like
this one.
Important update on ACM’s new open access publishing model for 2026 ACM
Conferences:
<https://icfp26.sigplan.org/track/icfp-2026-icfp-papers#important-update-on-acms-new-open-access-publishing-model-for-2026-acm-conferences>

Starting January 1, 2026, ACM will fully transition to Open Access. All ACM
publications, including those from ACM-sponsored conferences, will be 100%
Open Access. Authors will have two primary options for publishing Open
Access articles with ACM: the ACM Open institutional model or by paying
Article Processing Charges (APCs). With over 1,800 institutions already
part of ACM Open, the majority of ACM-sponsored conference papers will not
require APCs from authors or conferences (currently, around 70–75%).

Authors from institutions not participating in ACM Open will need to pay an
APC to publish their papers, unless they qualify for a geographic or
discretionary waiver. To find out whether an APC applies to your article,
please consult the list of participating institutions
<https://libraries.acm.org/acmopen/open-participants> in ACM Open and
review the APC Waivers and Discounts Policy
<https://www.acm.org/publications/policies/policy-on-open-access-apc-waivers-and-discounts>
.

To support a smooth transition and encourage broader ACM Open
participation, ACM has introduced a temporary subsidy on APC pricing for
2026, funded directly by ACM. This pricing applies to all articles
published in ACM and SIG sponsored conferences taking place in 2026. The
subsidized conference pricing for 2026 is as follows:
Authors No ACM or SIG members At least 1 ACM or SIG member
ACM and SIG Sponsored Conference Article $350 $250
>From a lower-middle-income country
<https://www.acm.org/publications/policies/lower-middle-income-countries>
$175 $125

This represents a 65% discount <https://www.acm.org/publications/openaccess>,
funded directly by ACM. Authors are encouraged to help advocate for their
institutions to join ACM Open during this transition period.

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

[MLton-user] [TFP 2026] 2nd Call for Papers for the 27th International Symposium on Trends in Functional Programming, Odense, Denmark, January 27-30 2026

['Peter A. v. MLton-u. <mlt...@ml...>]

# TFP 2026 - Second Call for Papers
(trendsfp.github.io)

## Important Dates

Submission deadline (pre-symposium, full papers): Thu 13th Nov 2025 
(AOE)
Notification        (pre-symposium, full papers): Thu 11th Dec 2025
Submission deadline (pre-symposium draft papers): Thu 11th Dec 2025 
(AOE)
Notification        (pre-symposium draft papers): Fri 19th Dec 2025
Symposium:                                        Tue 27th Jan - Thu 
30th Jan 2026 (TFPiE 26th Jan 2025)
Submission deadline (post-symposium review):      Thu  5th Mar 2026 
(AOE)
Notification        (post-symposium submissions): Thu 16th Apr 2026

The Symposium on Trends in Functional Programming (TFP) is an 
international
forum for researchers with interests in all aspects of functional 
programming,
taking a broad view of current and future trends in the area. It aspires 
to be a
lively environment for presenting the latest research results, and other
contributions.

This year, TFP will take place in-person at the University of Southern 
Denmark,
in Odense, Denmark. It is co-located with the Trends in Functional 
Programming
in Education (TFPIE) workshop, which will take on the day before the 
main
symposium.

Please be aware that TFP has several submission deadlines. The first, 
13th
November, is for authors who wish to have their full paper reviewed 
prior to the
symposium. Papers that are accepted in this way must also be presented 
at the
symposium. The second, 11th December, is for authors who wish to present 
their
work or work-in-progress at the symposium first without submitting to 
the full
review process for publication. These authors can then take into account
feedback received at the symposium and submit a full paper for review by 
the
third deadline, 5th March.

## Scope

The symposium recognizes that new trends may arise through various 
routes. As
part of the Symposium's focus on trends we therefore identify the 
following five
paper categories. High-quality submissions are solicited in any of these
categories:

*   Research Papers: Leading-edge, previously unpublished research work
*   Position Papers: On what new trends should or should not be
*   Project Papers: Descriptions of recently started new projects
*   Evaluation Papers: What lessons can be drawn from a finished project
*   Overview Papers: Summarizing work with respect to a trendy subject

Papers must be original and not simultaneously submitted for publication 
to any
other forum. They may consider any aspect of functional programming:
theoretical, implementation-oriented, or experience-oriented. 
Applications of
functional programming techniques to other languages are also within the 
scope
of the symposium.

Topics suitable for the symposium include, but are not limited to:

*   Functional programming and multicore/manycore computing
*   Functional programming in the cloud
*   High performance functional computing
*   Extra-functional (behavioural) properties of functional programs
*   Dependently typed functional programming
*   Validation and verification of functional programs
*   Debugging and profiling for functional languages
*   Functional programming in different application areas:
     security, mobility, telecommunications applications, embedded 
systems,
     global computing, grids, etc.
*   Interoperability with imperative programming languages
*   Novel memory management techniques
*   Program analysis and transformation techniques
*   Empirical performance studies
*   Abstract/virtual machines and compilers for functional languages
*   (Embedded) domain specific languages
*   New implementation strategies
*   Any new emerging trend in the functional programming area

If you are in doubt on whether your paper is within the scope of TFP, 
please
contact the programme chair, Casper Bach.

## Best Paper Awards

TFP awards two prizes for the best papers each year.

First, to reward excellent contributions, TFP awards a prize for the 
best
overall paper accepted for the post-conference formal proceedings.

Second, each year TFP also awards a prize for the best student paper. 
TFP
traditionally pays special attention to research students, acknowledging 
that
students are almost by definition part of new subject trends. A student 
paper is
one for which the authors state that the paper is mainly the work of 
students,
the students are the paper's first authors, and a student would present 
the
paper.

In both cases, it is the PC of TFP that awards the prize. In case the 
best paper
happens to be a student paper, then that paper will receive both prizes.

## Student and Early Career Scholarships

Our sponsors have generously offered to fund seven scholarships of DKK 
3000
(approximately USD 460) to cover expenses in connection with traveling 
to and
staying in Denmark in connection with the conference.

Information on how to apply for these scholarships will be available 
soon on
https://trendsfp.github.io/

## Instructions to Authors

Submission is via HotCRP:

   https://tfp26.hotcrp.com/

Authors of papers have the choice of having their contributions formally
reviewed either before or after the Symposium. Further, pre-symposium
submissions may either be full (earlier deadline) or draft papers (later
deadline).

## Pre-symposium formal review

Papers to be formally reviewed before the symposium should be submitted 
before
the early deadline and will receive their reviews and notification of 
acceptance
for both presentation and publication before the symposium. A paper that 
has
been rejected for publication but accepted for presentation may be 
revised and
resubmitted for the post-symposium formal review.

## Post-symposium formal review

Draft papers will receive minimal reviews and notification of acceptance 
for
presentation at the symposium. Authors of draft papers will be invited 
to submit
revised papers based on the feedback received at the symposium. A 
post-symposium
refereeing process will then select a subset of these papers for formal
publication.

## Paper categories

Draft papers and papers submitted for formal review are submitted as 
extended
abstracts (4 to 10 pages in length) or full papers (up to 20 pages). The
submission must clearly indicate which category it belongs to: research,
position, project, evaluation, or overview paper. It should also 
indicate which
authors are research students, and whether the main author(s) are 
students. A
draft paper for which all authors are students will receive additional 
feedback
by one of the PC members shortly after the symposium has taken place.

## Format

Papers must be written in English, and written using the LNCS style. For 
more
information about formatting please consult the Springer LNCS Guidelines 
web
site
(https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines).

## Organizing Committee

Casper Bach         University of Southern Denmark, DK  Programme Chair
Jeremy Gibbons      University of Oxford, UK            General Chair
Jason Hemann        Seton Hall University, US           Conference Chair
Peter Achten        Radboud University Nijmegen, NL     Publicity Chair
Marco T. Morazán    Seton Hall University, US           Steering 
Committee Chair

## Programme Committee

Alex Gerdes            University of Gothenburg and Chalmers, SE
Ben Greenman           University of Utah, US
Bruno Oliveira         University of Hong Kong, HK
Cas van der Rest       Shielded Technologies, NL
Cristina Matache       University of Edinburgh, UK
Eric Van Wyk           University of Minnesota, US
Jeremy Yallop          University of Cambridge, UK
Jules Jacobs           Cornell University, US
Mart Lubbers           Radboud University, NL
Max S. New             University of Michigan, US
Nicolas Wu             Imperial College London, UK
Patrick Bahr           IT University of Copenhagen, DK
Matthew Lutze          Aarhus University, DK
Dylan McDermott        University of Oxford, UK
Andrew Tolmach         Portland State University, US
Di Wang                Peking University, CN
Jesper Cockx           Delft University of Technology, NL
Jan de Muijnck-Hughes  Strathclyde, UK

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

Re: [MLton-user] [Polyml] tuple indexing: 0-based or 1-based?

[Andreas R. <ros...@mp...>]

> On 28. Oct 2025, at 03:29, David MacQueen <dma...@ma...> wrote:
> 
> This would be a good discussion to carry on at standardml.zulipchat.com!  I established that Zulip “organization” for just 
> such discussions, which may as well be carried out “in public” in some sense.
> 
> Anyway, my 2 cents about tuples:
> 
> In general mathematical discourse, I believe it is common to talk about the “first”, “second”, etc. element of a tuple,
> where a tuple is an element of an n-ary product (and where the product is typically homogenious, e.g.
> R * R * R, rather than R * I * B.  In ISWIM and LCF/ML, one uses the projection names “fst”, “snd” for projecting
> from a binary product (the only “arity” of product supported), which suggests numbering the components of
> a pair as 1 and 2.   We saw no point in diverging from this common practice in Standard ML; hence tuple projections
> are #1, #2, etc.
> 
> One SML design choice that I have come to feel uncomfortable about (perhaps I always did) is viewing tuples
> as records with natural number _labels_.  I.e. (3, true) = {1 = 3, 2 = true}.  This allows anomalous things like
> {1 = 3, 17 = true}, which is an odd sort of record with numberic labels but which is not a tuple.

I don’t see an issue with numeric records that don’t correspond to a tuple. But I always disliked the fact that numeric records contain seemingly absurd equations like `1 = 3`. That could easily be fixed by changing the syntax of numeric labels, e.g., to `_1` (or `~1` as OCaml would now, if you enjoy that particular syntax).

But we’re digressing. :)

As for tuple indexing in OCaml, the fact that OCaml itself already has functions named `fst` and `snd` perhaps is another good reason to stick to the 1-based convention.


>  In fact, in my
> planned New Front End project, I plan to break with this treatment and view tuples as standing on their own, not
> as special sorts of record.  Merging tuples into records produced some simplification in implementation (not having
> to support tuples per se in the abstract syntax, for instance), but at the cost of a bit of “tricky-ness”.  This issue is
> orthogonal about how we choose to number the elements of a tuple.
> 
> [By the way, I wrote the proposal on records and tuples during the SML design discussions.]
> 
> Dave
> 
> 
>> On Oct 27, 2025, at 7:47 AM, Gergely Buday <g....@sh...> wrote:
>> 
>> Yes, for order numbers it is more natural in plain English to use
>> first than zeroth.
>> 
>> Zero comes more naturally at e.g. a geometric sequence, a_i = a * q^n,
>> then a_0 = a, this is more natural. But in a tuple we do not compute
>> with the indices, they just select an element which might be some
>> other type than the other ones.
>> 
>> - Gergely
>> 
>> On Mon, 27 Oct 2025 at 14:25, Matthew Fluet <mat...@gm...> wrote:
>>> 
>>> I'm also in favor of 1-based tuples.  Adding one other argument: I've never seen an extension of the lambda calculus with pairs that introduces projects `zth` and `fst`; it's always `fst` and `snd`.
>>> 
>>> -Matthew
>>> 
>>> On Mon, Oct 27, 2025 at 4:46 AM Florian Weimer <fw...@de...> wrote:
>>>> 
>>>> * John Reppy:
>>>> 
>>>>> FYI, I think zero-based array indexing is an artifact of the fact
>>>>> that early C did not really have arrays; it just had syntactic sugar
>>>>> for pointer arithmetic.  Fortran had (has?) 1-based indices and
>>>>> Algol and Pascal had arbitrary base indices.
>>>> 
>>>> On the other hand, if your language supports array slices (non-copying
>>>> subarrays) and these slices preserve the original indices, you are
>>>> effectively back to zero-based indexing: you have to access relative
>>>> to the starting index of the slice, so the first element is at zero.
>>>> Ada is like that, array slice elements go from Slice (Slice'First),
>>>> Slice (Slice'First + 1) up to Slice (Slice'First + Slice'Length - 1).
>>>> This is a bit strange because Ada arrays start at index 1.
>>>> _______________________________________________
>>>> Poly/ML mailing list -- po...@li...
>>>> To unsubscribe send an email to pol...@li...
>>> 
>>> _______________________________________________
>>> Poly/ML mailing list -- po...@li...
>>> To unsubscribe send an email to pol...@li...
> 
> David MacQueen
> dma...@ma...
> 
> 

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

Re: [MLton-user] [Polyml] tuple indexing: 0-based or 1-based?

['David M. v. MLton-u. <mlt...@ml...>]

This would be a good discussion to carry on at standardml.zulipchat.com <http://standardml.zulipchat.com/>!  I established that Zulip “organization” for just 
such discussions, which may as well be carried out “in public” in some sense.

Anyway, my 2 cents about tuples:

In general mathematical discourse, I believe it is common to talk about the “first”, “second”, etc. element of a tuple,
where a tuple is an element of an n-ary product (and where the product is typically homogenious, e.g.
R * R * R, rather than R * I * B.  In ISWIM and LCF/ML, one uses the projection names “fst”, “snd” for projecting
from a binary product (the only “arity” of product supported), which suggests numbering the components of
a pair as 1 and 2.   We saw no point in diverging from this common practice in Standard ML; hence tuple projections
are #1, #2, etc.

One SML design choice that I have come to feel uncomfortable about (perhaps I always did) is viewing tuples
as records with natural number _labels_.  I.e. (3, true) = {1 = 3, 2 = true}.  This allows anomalous things like
{1 = 3, 17 = true}, which is an odd sort of record with numberic labels but which is not a tuple.  In fact, in my
planned New Front End project, I plan to break with this treatment and view tuples as standing on their own, not
as special sorts of record.  Merging tuples into records produced some simplification in implementation (not having
to support tuples per se in the abstract syntax, for instance), but at the cost of a bit of “tricky-ness”.  This issue is
orthogonal about how we choose to number the elements of a tuple.

[By the way, I wrote the proposal on records and tuples during the SML design discussions.]

Dave


> On Oct 27, 2025, at 7:47 AM, Gergely Buday <g....@sh...> wrote:
> 
> Yes, for order numbers it is more natural in plain English to use
> first than zeroth.
> 
> Zero comes more naturally at e.g. a geometric sequence, a_i = a * q^n,
> then a_0 = a, this is more natural. But in a tuple we do not compute
> with the indices, they just select an element which might be some
> other type than the other ones.
> 
> - Gergely
> 
> On Mon, 27 Oct 2025 at 14:25, Matthew Fluet <mat...@gm...> wrote:
>> 
>> I'm also in favor of 1-based tuples.  Adding one other argument: I've never seen an extension of the lambda calculus with pairs that introduces projects `zth` and `fst`; it's always `fst` and `snd`.
>> 
>> -Matthew
>> 
>> On Mon, Oct 27, 2025 at 4:46 AM Florian Weimer <fw...@de...> wrote:
>>> 
>>> * John Reppy:
>>> 
>>>> FYI, I think zero-based array indexing is an artifact of the fact
>>>> that early C did not really have arrays; it just had syntactic sugar
>>>> for pointer arithmetic.  Fortran had (has?) 1-based indices and
>>>> Algol and Pascal had arbitrary base indices.
>>> 
>>> On the other hand, if your language supports array slices (non-copying
>>> subarrays) and these slices preserve the original indices, you are
>>> effectively back to zero-based indexing: you have to access relative
>>> to the starting index of the slice, so the first element is at zero.
>>> Ada is like that, array slice elements go from Slice (Slice'First),
>>> Slice (Slice'First + 1) up to Slice (Slice'First + Slice'Length - 1).
>>> This is a bit strange because Ada arrays start at index 1.
>>> _______________________________________________
>>> Poly/ML mailing list -- po...@li...
>>> To unsubscribe send an email to pol...@li...
>> 
>> _______________________________________________
>> Poly/ML mailing list -- po...@li...
>> To unsubscribe send an email to pol...@li...

David MacQueen
dma...@ma...


To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

Re: [MLton-user] [Polyml] Re: tuple indexing: 0-based or 1-based?

['Gergely B. v. MLton-u. <mlt...@ml...>]

Yes, for order numbers it is more natural in plain English to use
first than zeroth.

Zero comes more naturally at e.g. a geometric sequence, a_i = a * q^n,
then a_0 = a, this is more natural. But in a tuple we do not compute
with the indices, they just select an element which might be some
other type than the other ones.

- Gergely

On Mon, 27 Oct 2025 at 14:25, Matthew Fluet <mat...@gm...> wrote:
>
> I'm also in favor of 1-based tuples.  Adding one other argument: I've never seen an extension of the lambda calculus with pairs that introduces projects `zth` and `fst`; it's always `fst` and `snd`.
>
> -Matthew
>
> On Mon, Oct 27, 2025 at 4:46 AM Florian Weimer <fw...@de...> wrote:
>>
>> * John Reppy:
>>
>> > FYI, I think zero-based array indexing is an artifact of the fact
>> > that early C did not really have arrays; it just had syntactic sugar
>> > for pointer arithmetic.  Fortran had (has?) 1-based indices and
>> > Algol and Pascal had arbitrary base indices.
>>
>> On the other hand, if your language supports array slices (non-copying
>> subarrays) and these slices preserve the original indices, you are
>> effectively back to zero-based indexing: you have to access relative
>> to the starting index of the slice, so the first element is at zero.
>> Ada is like that, array slice elements go from Slice (Slice'First),
>> Slice (Slice'First + 1) up to Slice (Slice'First + Slice'Length - 1).
>> This is a bit strange because Ada arrays start at index 1.
>> _______________________________________________
>> Poly/ML mailing list -- po...@li...
>> To unsubscribe send an email to pol...@li...
>
> _______________________________________________
> Poly/ML mailing list -- po...@li...
> To unsubscribe send an email to pol...@li...

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

Re: [MLton-user] [Polyml] Re: tuple indexing: 0-based or 1-based?

[Matthew F. <mat...@gm...>]

I'm also in favor of 1-based tuples.  Adding one other argument: I've never
seen an extension of the lambda calculus with pairs that introduces
projects `zth` and `fst`; it's always `fst` and `snd`.

-Matthew

On Mon, Oct 27, 2025 at 4:46 AM Florian Weimer <fw...@de...> wrote:

> * John Reppy:
>
> > FYI, I think zero-based array indexing is an artifact of the fact
> > that early C did not really have arrays; it just had syntactic sugar
> > for pointer arithmetic.  Fortran had (has?) 1-based indices and
> > Algol and Pascal had arbitrary base indices.
>
> On the other hand, if your language supports array slices (non-copying
> subarrays) and these slices preserve the original indices, you are
> effectively back to zero-based indexing: you have to access relative
> to the starting index of the slice, so the first element is at zero.
> Ada is like that, array slice elements go from Slice (Slice'First),
> Slice (Slice'First + 1) up to Slice (Slice'First + Slice'Length - 1).
> This is a bit strange because Ada arrays start at index 1.
> _______________________________________________
> Poly/ML mailing list -- po...@li...
> To unsubscribe send an email to pol...@li...
>

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

Re: [MLton-user] [Polyml] Re: tuple indexing: 0-based or 1-based?

[Florian W. <fw...@de...>]

* John Reppy:

> FYI, I think zero-based array indexing is an artifact of the fact
> that early C did not really have arrays; it just had syntactic sugar
> for pointer arithmetic.  Fortran had (has?) 1-based indices and
> Algol and Pascal had arbitrary base indices.

On the other hand, if your language supports array slices (non-copying
subarrays) and these slices preserve the original indices, you are
effectively back to zero-based indexing: you have to access relative
to the starting index of the slice, so the first element is at zero.
Ada is like that, array slice elements go from Slice (Slice'First),
Slice (Slice'First + 1) up to Slice (Slice'First + Slice'Length - 1).
This is a bit strange because Ada arrays start at index 1.

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

Re: [MLton-user] tuple indexing: 0-based or 1-based?

[John R. <jh...@cs...>]

> On Oct 25, 2025, at 19:32, Gabriel Scherer <gab...@in...> wrote:
> 
> Dear SML people,
> 
> There is an OCaml feature proposal by Alistair O'Brien that would finally introduce tuple indexing in OCaml -- we currently have only whole-tuple pattern matching:
> 
>  RFC: https://github.com/johnyob/ocaml-RFCs/blob/tuple-projections/rfcs/tuple_projections.md
>  discussion: https://github.com/ocaml/RFCs/pull/57
> 
> Of course this raises the Very Important Question of whether indexing should be 0-based or 1-based.
> 
> The argument in favor of 0-based is that it is what we use for arrays, so more consistent, standard in most programming languages. The argument in favor of 1-based is that it is arguably more intuitive (but the inconsistency with arrays weakens this claim noticeably), and that SML uses it.
> 
> Question: you have a lot more experience using tuple indexing. In your opinion, if this was to be decided again for a new system (no backward-compatibility concerns), would you still recommend using 1-based indices, or would you be more in favor of 0-based indices?

I think that base-1 indexing makes more sense, since it matches the usual projection/indexing found in common
mathematical usage.  I think tuples and arrays are pretty different, so I don't see consistency as being crucial.
You are not going to be doing index arithmetic on tuple indices, they are really just labels.

FYI, I think zero-based array indexing is an artifact of the fact that early C did not really have arrays; it just had
syntactic sugar for pointer arithmetic.  Fortran had (has?) 1-based indices and Algol and Pascal had arbitrary base
indices.

> 
> 
> 
> P.S.: You may be amused to learn that OCaml recently introduced "labeled tuples" (looking like `(x:1, y:2)` in expressions and `(x:int * y:int)` in types), which are basically a restricted version of SML structural records -- type inference does not try very hard and requires an annotation in practice.
> 
> P.P.S: Is there still a mailing-list for the SML/NJ crowd? All I could find were github discussions (https://github.com/orgs/smlnj/discussions) and an invite-only Zulip.

The sml...@ma... <mailto:sml...@ma...> list is still used to announce releases, but we've mostly switched to using GitHub
for communication.  David MacQueen manages the Zulip, which I don't follow very closely.

	- John


To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

Re: [MLton-user] [Polyml] tuple indexing: 0-based or 1-based?

[Makarius <mak...@sk...>]

On 25/10/2025 14:32, Gabriel Scherer wrote:
> 
> The argument in favor of 0-based is that it is what we use for arrays, so more 
> consistent, standard in most programming languages. The argument in favor of 
> 1-based is that it is arguably more intuitive (but the inconsistency with 
> arrays weakens this claim noticeably), and that SML uses it.
> 
> Question: you have a lot more experience using tuple indexing. In your 
> opinion, if this was to be decided again for a new system (no backward- 
> compatibility concerns), would you still recommend using 1-based indices, or 
> would you be more in favor of 0-based indices?

I am normally a purist in counting almost everything from 0, but for tuples I 
would not do it. It just asking for too much trouble, in conflict with usual 
mathematical customs like (x1, x2, x3, x4) etc. Think of old-fashioned vectors 
and matrices.

Speaking abstractly, consistency is a high value not to be given up lightly, 
but there are often situations, where special rules should apply to a certain 
"curpus separatum".


	Makarius

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

Re: [MLton-user] tuple indexing: 0-based or 1-based?

[Andreas R. <ros...@mp...>]

Yay to that!!

>From my perspective, the main reason in favour of 1-based is that programmers almost universally write

    let f (x1, x2) = ...

today, so the 1-based convention already is everywhere. IME it's quite confusing when such code is mixed with uses of a projection operator based on a different numbering scheme, which is inevitable in practice.

The comparison with arrays is less important IMO, since tuple indices are just static names and not computed, so rather different beasts.

That said, I don’t have a super-strong opinion here, just give me e.i already. :)

Cheers,
/Andreas


> On 25. Oct 2025, at 14:32, Gabriel Scherer <gab...@in...> wrote:
> 
> Dear SML people,
> 
> There is an OCaml feature proposal by Alistair O'Brien that would finally introduce tuple indexing in OCaml -- we currently have only whole-tuple pattern matching:
> 
>  RFC: https://github.com/johnyob/ocaml-RFCs/blob/tuple-projections/rfcs/tuple_projections.md
>  discussion: https://github.com/ocaml/RFCs/pull/57
> 
> Of course this raises the Very Important Question of whether indexing should be 0-based or 1-based.
> 
> The argument in favor of 0-based is that it is what we use for arrays, so more consistent, standard in most programming languages. The argument in favor of 1-based is that it is arguably more intuitive (but the inconsistency with arrays weakens this claim noticeably), and that SML uses it.
> 
> Question: you have a lot more experience using tuple indexing. In your opinion, if this was to be decided again for a new system (no backward-compatibility concerns), would you still recommend using 1-based indices, or would you be more in favor of 0-based indices?
> 
> 
> 
> P.S.: You may be amused to learn that OCaml recently introduced "labeled tuples" (looking like `(x:1, y:2)` in expressions and `(x:int * y:int)` in types), which are basically a restricted version of SML structural records -- type inference does not try very hard and requires an annotation in practice.
> 
> P.P.S: Is there still a mailing-list for the SML/NJ crowd? All I could find were github discussions (https://github.com/orgs/smlnj/discussions) and an invite-only Zulip.

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

[MLton-user] tuple indexing: 0-based or 1-based?

[Gabriel S. <gab...@in...>]

Dear SML people,

There is an OCaml feature proposal by Alistair O'Brien that would 
finally introduce tuple indexing in OCaml -- we currently have only 
whole-tuple pattern matching:

   RFC: 
https://github.com/johnyob/ocaml-RFCs/blob/tuple-projections/rfcs/tuple_projections.md
   discussion: https://github.com/ocaml/RFCs/pull/57

Of course this raises the Very Important Question of whether indexing 
should be 0-based or 1-based.

The argument in favor of 0-based is that it is what we use for arrays, 
so more consistent, standard in most programming languages. The argument 
in favor of 1-based is that it is arguably more intuitive (but the 
inconsistency with arrays weakens this claim noticeably), and that SML 
uses it.

Question: you have a lot more experience using tuple indexing. In your 
opinion, if this was to be decided again for a new system (no 
backward-compatibility concerns), would you still recommend using 
1-based indices, or would you be more in favor of 0-based indices?



P.S.: You may be amused to learn that OCaml recently introduced "labeled 
tuples" (looking like `(x:1, y:2)` in expressions and `(x:int * y:int)` 
in types), which are basically a restricted version of SML structural 
records -- type inference does not try very hard and requires an 
annotation in practice.

P.P.S: Is there still a mailing-list for the SML/NJ crowd? All I could 
find were github discussions (https://github.com/orgs/smlnj/discussions) 
and an invite-only Zulip.

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

Re: [MLton-user] MLton uninstallation

[Matthew F. <mat...@gm...>]

We don't seem to have an uninstall target in either the source or binary
distribution Makefiles.  Might be worth adding.

But, I believe that the following will uninstall all of the installed files:

  rm /usr/local/bin/mlton
  rm /usr/local/bin/mllex
  rm /usr/local/bin/mlyacc
  rm /usr/local/bin/mlprof
  rm /usr/local/bin/mlnlffigen
  rm -rf /usr/local/lib/mlton
  rm -rf /usr/local/share/doc/mlton
  rm /usr/local/share/man/man1/mlton
  rm /usr/local/share/man/man1/mllex
  rm /usr/local/share/man/man1/mlyacc
  rm /usr/local/share/man/man1/mlprof
  rm /usr/local/share/man/man1/mlnlffigen





On Fri, Oct 17, 2025 at 3:22 PM Arnav Sabharwal <arn...@an...>
wrote:

> Hello,
>
> What is the canonical way to uninstall MLton? I installed it per the
> (only) way described in the repository.
>
> Thanks,
> Arnav Sabharwal.
>
> To unsubscribe from this group and stop receiving emails from it, send an
> email to mlt...@ml....
> _______________________________________________
> MLton-user mailing list
> MLt...@li...; mlt...@ml...
> https://lists.sourceforge.net/lists/listinfo/mlton-user
>

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

[MLton-user] MLton uninstallation

[Arnav S. <arn...@an...>]

Hello,

What is the canonical way to uninstall MLton? I installed it per the (only)
way described in the repository.

Thanks,
Arnav Sabharwal.

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

[MLton-user] [TFP 2026] Call for Papers for the 27th International Symposium on Trends in Functional Programming, Odense, Denmark, January 2026

['Peter A. v. MLton-u. <mlt...@ml...>]

# TFP 2026 -- Call for Papers
(trendsfp.github.io)

## Important Dates

* Submission deadline (pre-symposium, full papers): Thu 13th Nov 2025 
(AOE)
* Notification        (pre-symposium, full papers): Thu 11th Dec 2025
* Submission deadline (pre-symposium draft papers): Thu 11th Dec 2025 
(AOE)
* Notification        (pre-symposium draft papers): Fri 19th Dec 2025
* Submission deadline (post-symposium review):      Thu  5th Mar 2026 
(AOE)
* Notification        (post-symposium submissions): Thu 16th Apr 2026

The Symposium on Trends in Functional Programming (TFP) is an 
international
forum for researchers with interests in all aspects of functional 
programming,
taking a broad view of current and future trends in the area. It aspires 
to be a
lively environment for presenting the latest research results, and other
contributions.

This year, TFP will take place in-person at the University of Southern 
Denmark,
in Odense, Denmark. It is co-located with the Trends in Functional 
Programming
in Education (TFPIE) workshop, which will take on the day before the 
main
symposium.

Please be aware that TFP has several submission deadlines. The first, 
13th
November, is for authors who wish to have their full paper reviewed 
prior to the
symposium. Papers that are accepted in this way must also be presented 
at the
symposium. The second, 11th December, is for authors who wish to present 
their
work or work-in-progress at the symposium first without submitting to 
the full
review process for publication. These authors can then take into account
feedback received at the symposium and submit a full paper for review by 
the
third deadline, 19th February.

## Scope

The symposium recognizes that new trends may arise through various 
routes. As
part of the Symposium's focus on trends we therefore identify the 
following five
paper categories. High-quality submissions are solicited in any of these
categories:

*   Research Papers: Leading-edge, previously unpublished research work
*   Position Papers: On what new trends should or should not be
*   Project Papers: Descriptions of recently started new projects
*   Evaluation Papers: What lessons can be drawn from a finished project
*   Overview Papers: Summarizing work with respect to a trendy subject

Papers must be original and not simultaneously submitted for publication 
to any
other forum. They may consider any aspect of functional programming:
theoretical, implementation-oriented, or experience-oriented. 
Applications of
functional programming techniques to other languages are also within the 
scope
of the symposium.

Topics suitable for the symposium include, but are not limited to:

*   Functional programming and multicore/manycore computing
*   Functional programming in the cloud
*   High performance functional computing
*   Extra-functional (behavioural) properties of functional programs
*   Dependently typed functional programming
*   Validation and verification of functional programs
*   Debugging and profiling for functional languages
*   Functional programming in different application areas:
     security, mobility, telecommunications applications, embedded 
systems,
     global computing, grids, etc.
*   Interoperability with imperative programming languages
*   Novel memory management techniques
*   Program analysis and transformation techniques
*   Empirical performance studies
*   Abstract/virtual machines and compilers for functional languages
*   (Embedded) domain specific languages
*   New implementation strategies
*   Any new emerging trend in the functional programming area

If you are in doubt on whether your paper is within the scope of TFP, 
please
contact the programme chair, Casper Bach.

## Best Paper Awards

TFP awards two prizes for the best papers each year.

First, to reward excellent contributions, TFP awards a prize for the 
best
overall paper accepted for the post-conference formal proceedings.

Second, each year TFP also awards a prize for the best student paper. 
TFP
traditionally pays special attention to research students, acknowledging 
that
students are almost by definition part of new subject trends. A student 
paper is
one for which the authors state that the paper is mainly the work of 
students,
the students are the paper's first authors, and a student would present 
the
paper.

In both cases, it is the PC of TFP that awards the prize. In case the 
best paper
happens to be a student paper, then that paper will receive both prizes.

## Instructions to Authors

Submission is via HotCRP:

   https://tfp26.hotcrp.com/

Authors of papers have the choice of having their contributions formally
reviewed either before or after the Symposium. Further, pre-symposium
submissions may either be full (earlier deadline) or draft papers (later
deadline). See below for more details.

Submission is single-blind.

Submissions are welcome from PC members (except the chair).

Accepted papers from the pre-symposium and post-symposium formal review 
will
appear in a formal proceedings, published by Springer.

Papers must be written in English, and written using the LNCS style. For 
more
information about formatting please consult the Springer LNCS Guidelines 
web
site
(https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines).

### Pre-symposium formal review

Papers to be formally reviewed before the symposium should be submitted 
before
the early deadline and will receive their reviews and notification of 
acceptance
for both presentation and publication before the symposium. A paper that 
has
been rejected for publication but accepted for presentation may be 
revised and
resubmitted for the post-symposium formal review.

### Post-symposium formal review

Draft papers will receive minimal reviews and notification of acceptance 
for
presentation at the symposium. Authors of draft papers will be invited 
to submit
revised papers based on the feedback received at the symposium. A 
post-symposium
refereeing process will then select a subset of these papers for formal
publication.

### Paper categories

Draft papers and papers submitted for formal review are submitted as 
extended
abstracts (4 to 10 pages in length) or full papers (up to 20 pages). The
submission must clearly indicate which category it belongs to: research,
position, project, evaluation, or overview paper. It should also 
indicate which
authors are research students, and whether the main author(s) are 
students. A
draft paper for which all authors are students will receive additional 
feedback
by one of the PC members shortly after the symposium has taken place.

## Organizing Committee

| Casper Bach      | University of Southern Denmark, DK | Programme 
Chair          |
| Jeremy Gibbons   | University of Oxford               | General Chair  
           |
| Peter Achten     | Radboud University Nijmegen, NL    | Publicity 
Chair          |
| Marco T. Morazán | Seton Hall University, US          | Steering 
Committee Chair |

## Programme Committee

| Alex Gerdes          | University of Gothenburg and Chalmers, SE |
| Andrew Tolmach       | Portland State University, US             |
| Ben Greenman         | University of Utah, US                    |
| Bruno Oliveira       | University of Hong Kong, HK               |
| Cas van der Rest     | Shielded Technologies, NL                 |
| Cristina Matache     | University of Edinburgh, UK               |
| Di Wang              | Peking University, CN                     |
| Dylan McDermott      | University of Oxford, UK                  |
| Eric Van Wyk         | University of Minnesota, US               |
| Jan de Muijnck-Hughe | Strathclyde, UK                           |
| Jeremy Yallop        | University of Cambridge, UK               |
| Jesper Cockx         | Delft University of Technology, NL        |
| Jules Jacobs         | Cornell University, US                    |
| Mart Lubbers         | Radboud University, NL                    |
| Matthew Lutze        | Aarhus University, DK                     |
| Max S. New           | University of Michigan, US                |
| Nicolas Wu           | Imperial College London, UK               |
| Patrick Bahr         | IT University of Copenhagen, DK           |

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

[MLton-user] ICFP 2025 (Co-Located with SPLASH!): Call for Participation

['ICFP P. v. MLton-u. <mlt...@ml...>]

==================================================
Call for Participation

The 30th ACM SIGPLAN International Conference
on Functional Programming (ICFP 2025) and
affiliated events

*** This year, co-located with SPLASH for a ***
*** joint ICFP/SPLASH Conference ***

https://icfp25.sigplan.org
Singapore; Oct 12-18, 2025

*** Register by Aug 31, 2025 for a discount! ***
==================================================

ICFP is a celebration of the art and science of
functional programming, providing a forum for
researchers and developers to engage on a variety
of topics, from foundations to features, and from
abstraction to application.

This year, for the first time in history, ICFP will
be co-located with SPLASH and its satellite events
as a part of the joint ICFP/SPLASH 2025 conference.

You are invited to participate in a full week of
events dedicated to the art and science of programming,
featuring both the ICFP and SPLASH main conferences
as well as numerous related events.

* ICFP Accepted Papers:
https://icfp25.sigplan.org/track/icfp-2025-papers#event-overview

* Registration:
https://icfp25.sigplan.org/attending/registration
*The early-bird deadline is August 31, 2025*
(Additionally, there is a full week discount
if you register for 7 days!)

* Venue (Sunday Workshops only): NUS School of Computing
https://icfp25.sigplan.org/venue/splash-2025-venue1

* Venue (Main Conference): Marina Bay Sands Convention Centre
https://icfp25.sigplan.org/venue/splash-2025-venue


Full list of events:

October 12
Tutorials
-
https://conf.researchr.org/track/icfp-splash-2025/icfp-splash-2025-tutorials
PLMW
- https://conf.researchr.org/home/icfp-splash-2025/plmw-icfp-splash-2025
TyDE
- https://conf.researchr.org/home/icfp-splash-2025/tyde-2025
FARM
- https://2025.splashcon.org/track/splash-2025-farm
HOPE
- https://conf.researchr.org/home/icfp-splash-2025/hope-2025
Erlang
- https://conf.researchr.org/home/icfp-splash-2025/erlang-2025
FUNARCH
- https://conf.researchr.org/home/icfp-splash-2025/funarch-2025

October 13-15
ICFP (3 days)
- https://icfp25.sigplan.org/

October 13-14
SAS (2 days)
- https://2025.splashcon.org/home/sas-2025

October 13
SPLASH Doctoral Symposium
- https://2025.splashcon.org/track/splash-2025-Doctoral-Symposium
SCALA
- https://conf.researchr.org/home/icfp-splash-2025/scala-2025
PROPL
- https://conf.researchr.org/home/icfp-splash-2025/propl-2025

October 14-15
OlivierFest (2 days)
- https://conf.researchr.org/home/icfp-splash-2025/olivierfest-2025
October 14
HATRA
- https://conf.researchr.org/home/icfp-splash-2025/hatra-2025
MPLR
- https://conf.researchr.org/home/icfp-splash-2025/mplr-2025
IWACO
- https://conf.researchr.org/home/icfp-splash-2025/iwaco-2025
October 15
PAINT
- https://conf.researchr.org/home/icfp-splash-2025/paint-2025
LMPL
- https://conf.researchr.org/home/icfp-splash-2025/lmpl-2025
VMIL
- https://conf.researchr.org/home/icfp-splash-2025/vmil-2025

October 16-18
OOPSLA (3 days)
- https://2025.splashcon.org/track/OOPSLA
ONWARD! (3 days)
- https://2025.splashcon.org/track/splash-2025-Onward-papers

October 16-17
HASKELL (2 days)
- https://conf.researchr.org/home/icfp-splash-2025/haskellsymp-2025

October 16
ML Family
- https://conf.researchr.org/home/icfp-splash-2025/mlsymposium-2025
SCHEME
- https://conf.researchr.org/home/icfp-splash-2025/scheme-2025
WASM
- https://conf.researchr.org/home/icfp-splash-2025/webassembly-ws-2025

October 17
OCAML
- https://conf.researchr.org/home/icfp-splash-2025/ocaml-2025
MINI KANREN
- https://conf.researchr.org/home/icfp-splash-2025/minikanren-2025
October 18
SPLASH-E
- https://2025.splashcon.org/track/splash-2025-SPLASH-E
REBASE
- https://conf.researchr.org/home/icfp-splash-2025/rebase-2025
Industry Forum
- https://conf.researchr.org/home/icfp-splash-2025/industry-forum-2025


ICFP 2025 will feature three keynotes:

Ekaterina Komendantskaya:
Proof-Carrying Neuro-Symbolic Code
https://icfp25.sigplan.org/details/icfp-2025-icfp-keynotes/2/Proof-Carrying-Neuro-Symbolic-Code

Christos Dimoulas:
The Rational Programmer, A Method for Investigating Programming Language
Pragmatics
https://icfp25.sigplan.org/details/icfp-2025-icfp-keynotes/3/The-Rational-Programmer-A-Method-for-Investigating-Programming-Language-Pragmatics

Satnam Singh:
Functional Programming for Hardware Design
https://icfp25.sigplan.org/details/icfp-2025-icfp-keynotes/1/Functional-Programming-for-Hardware-Design


ICFP 2025 conference organizers:

https://icfp25.sigplan.org/committee/icfp-2025-organizing-committee


We hope to see you in Singapore in October. Don't forget
to register by *August 31, 2025* for the early-bird
discount! Additionally, there is a *full-week discount*:
register for the whole 7 days and only pay for 6!

https://icfp25.sigplan.org/attending/registration

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

Re: [MLton-user] Interplay between empty datatypes and monomorphisation

[Matthew F. <mat...@gm...>]

You could use the CoreML IR, but (as a whole-program compiler), MLton will
always give you the CoreML IR for the whole program, so you'll need to
"find" your datatypes within there.

I'm not sure about the complexity of SML datatype definitions that you
expect to encounter, but I suspect that it might be simpler to just write
your own tiny parser for SML type definitions (and assume that the
complexities of type definitions aren't really used).  I kind of see the
appeal of the type-level "marking" of types in the datatypes, but I wonder
if a simple custom comment syntax might suffice:

```
datatype 'a tree = Leaf | Node of 'a tree * 'a * 'a tree
type iitree = (*#1*) ((*#0*) int tree) tree
```

I note that in your original example, you used a `type` definition to
describe the type of data to be generated, but note that elaboration to
CoreML has completely expanded all `type` definitions, so there wouldn't be
one to find in the CoreML program.

I suppose that in a larger application, it would be convenient to have all
of the datatype definitions available, but you will still need to parse the
CoreML sufficiently to find all of the involved types.

-Matthew


On Fri, Jul 25, 2025 at 9:41 PM Arnav Sabharwal <arn...@an...>
wrote:

> Hello Prof. Matthew, Yawar,
>
> Thank you for your response and advice! Apologies, I miscommunicated
> earlier: my OCaml "generator" (not generator - generator) takes in an SML
> type and the user specified target sizes for each involved inductive type
> and yields an SML term of said type, which meets the size constraints.
>
> I was considering the approach of stopping MLton at **some** point since:
>
>    1. I was hoping I could get MLton to unique-ify type variables for me
>    2. MLton could simplify the grammar of type and datatype declarations
>    for me, making parsing easier (as compared to say, parsing SML from source)
>
> Seemingly, the Core-ML IR seems to have these properties? Please correct
> me if I'm wrong!
>
> Thanks,
> Arnav.
>
> On Thu, Jul 24, 2025 at 9:21 PM Matthew Fluet <mat...@gm...>
> wrote:
>
>> Aranav isn’t subscribed, so I needed to moderate/accept the email before
>> it was sent to the whole list.
>>
>> On Thu, Jul 24, 2025 at 8:03 PM 'Yawar Raza (RIT Student)' via MLton-user
>> <mlt...@ml...> wrote:
>>
>>> Nevermind to my first paragraph. I just received the original email.
>>> Apparently they can get sent to me out of order...
>>>
>>> On Thursday, July 24, 2025, Yawar Raza (RIT Student) <ys...@ri...>
>>> wrote:
>>>
>>>> Arnav, I think you might need to use "Reply-All" for the reply to
>>>> remain on the mailing list, as only Prof. Fluet got your second email (I
>>>> didn't get it, at least).
>>>>
>>>> Anyway, I don't think "stopping the MLton compiler part way through" is
>>>> the best way to do the sort of thing you're trying to do.
>>>>
>>>> Something you _could_ look into is this one family of SML tricks
>>>> centered around http://mlton.org/Fold, possibly more specifically
>>>> http://mlton.org/VariableArityPolymorphism. I don't really understand
>>>> these libraries though, and I'm personally very averse to this sort of code.
>>>>
>>>> I don't really get what you're trying to do. Why do you have a
>>>> generator-generator? Is the generator (output by the generator-generator)
>>>> in SML itself or does it just output SML? Does it output just datatype
>>>> declarations or complete programs? I think saying what each level inputs
>>>> and outputs would be helpful.
>>>>
>>>> In general, you should probably end up doing one of the following:
>>>> - Push arity-polymorphism or similarly un-simple stuff up one generator
>>>> level, generating different SML source code text for each (rather than
>>>> trying to extract MLton compiler output).
>>>> - Give up on perfect type safety relating to arities, and just have the
>>>> different arities of some things share a single general type.
>>>> - Use a different language that either has dependent types (e.g. Idris)
>>>> or has more featureful metaprogramming (e.g. F# with its type providers).
>>>>
>>>> But maybe I'm just misunderstanding something. Feel free to ignore
>>>> those last two paragraph if so, but I hope those two MLton links above were
>>>> useful to learn exist, at least.
>>>>
>>>>
>>>> On Thursday, July 24, 2025, Matthew Fluet <mat...@gm...>
>>>> wrote:
>>>>>
>>>>> Well, if you just want a somewhat normalized representation of the
>>>>> types, then you might just use the CoreML representation immediately after
>>>>> elaboration (`-keep-pass parseAndElaborate`).
>>>>>
>>>>> For example:
>>>>> ```
>>>>> $ cat z.sml
>>>>> datatype zero = Zero
>>>>> datatype 'n succ = Succ
>>>>>
>>>>> datatype ('elem, 'index) my_list = Nil | Cons of 'elem * ('elem,
>>>>> 'index) my_list
>>>>> val z : ((int, zero) my_list, zero succ) my_list = raise Fail "todo"
>>>>> $ mlton -keep-pass parseAndElaborate z.sml
>>>>> $ tail z.parseAndElaborate.post.core-ml
>>>>> (* deadCode: true *)
>>>>> (* deadCode: true *)
>>>>> (* deadCode: false *)
>>>>> datatype zero_21 = Zero_0
>>>>> datatype 'a_4547 succ_2 = Succ_0
>>>>> datatype ('a_4549, 'a_4548) my_list_0 = Nil_0
>>>>>                                         | Cons_0 of 'a_4549
>>>>>                                                     * ('a_4549,
>>>>> 'a_4548) my_list_0
>>>>> val z_26: ((int32, zero_21) my_list_0, zero_21 succ_2) my_list_0 =
>>>>>    raise (Fail_0 "todo")
>>>>> ```
>>>>>
>>>>> But, note, you'll still need to see through the uniquification of all
>>>>> identifiers.
>>>>>
>>>>> -Matthew
>>>>>
>>>>> On Thu, Jul 24, 2025 at 10:48 AM Arnav Sabharwal <
>>>>> arn...@an...> wrote:
>>>>>
>>>>>> Hello Matthew,
>>>>>>
>>>>>> Thank you for your response! My larger goal here is to make a random
>>>>>> generator for (regular) SML inductive types that allows the user to
>>>>>> configure "target sizes" for every inductive structure within their type.
>>>>>> The type labels are meant to be a way for the user and the tool to agree on
>>>>>> a common language for referring to said inductive types.
>>>>>>
>>>>>> For example, say the user wants to generate 2-d lists where the outer
>>>>>> list has length 3 and each inner list has length 2. Then, they'd define
>>>>>> their list type like so, building towards their monomorphic "final" type:
>>>>>> ```
>>>>>> datatype ('elem, 'index) my_list = Nil | Cons of 'elem * ('elem,
>>>>>> 'index) my_list
>>>>>> type final = ((int, zero) my_list, zero succ) my_list
>>>>>> ```
>>>>>> This way, the user could later provide the lengths [2, 3] and the
>>>>>> tool would unambiguously be able to generate the type with the
>>>>>> specified constraints.
>>>>>>
>>>>>> Oh, and I'm writing the "random generator"-generator tool in OCaml.
>>>>>> So, I suppose one way could be to parse out the data-type and type
>>>>>> declarations from source, while these tags still hang around. But then I'd
>>>>>> have to "evaluate" type applications to bring them into a normal form, due
>>>>>> to the lingering type variables...which is why I was considering delaying
>>>>>> the point at which I "parse into an OCaml representation" as much as
>>>>>> possible.
>>>>>>
>>>>>> Happy to clarify more if necessary, would greatly appreciate your
>>>>>> advice!
>>>>>>
>>>>>> Arnav.
>>>>>>
>>>>>> On Thu, Jul 24, 2025 at 8:57 AM Matthew Fluet <
>>>>>> mat...@gm...> wrote:
>>>>>>
>>>>>>> Arnav,
>>>>>>>
>>>>>>> Yes, in SXML ("Simply-typed" XML), there is no polymorphism
>>>>>>> whatsoever (for functions or datatypes) and type parameters that do not
>>>>>>> contribute to the representation of a datatype will have been eliminated.
>>>>>>>
>>>>>>> Actually, the SimplfyTypes (http://mlton.org/XMLSimplifyTypes) XML
>>>>>>> optimization will have already eliminated these unused type parameters,
>>>>>>> before monomorphisation.  The motivation for SimplifyTypes is to avoid code
>>>>>>> duplication by monomorphisation that is unnecessary, due to type parameters
>>>>>>> that may be present for high-level API reasons, but do not affect the
>>>>>>> dynamics because they do not influence the data representation.
>>>>>>>
>>>>>>> It may be that if you drop SimplifyTypes (compile with `-drop-pass
>>>>>>> xmlSimplifyTypes`), then monomorphisation will force different "versions"
>>>>>>> of your tagged datatypes to be separately monmorphised, though with the
>>>>>>> current heuristics for naming monomorphised variants, you probably won't
>>>>>>> get any evidence of the `zero` or `succ` type parameters remaining in the
>>>>>>> SXML program.
>>>>>>>
>>>>>>> Could you say a bit more about your goals?  That might help to
>>>>>>> inform whether there is a better way to accomplish what you are trying to
>>>>>>> do.
>>>>>>>
>>>>>>> -Matthew
>>>>>>>
>>>>>>> On Thu, Jul 24, 2025 at 5:24 AM Arnav Sabharwal <
>>>>>>> arn...@an...> wrote:
>>>>>>>
>>>>>>>> Hello,
>>>>>>>>
>>>>>>>> I'm trying to tag every instance of a recursive type in a type
>>>>>>>> definition with a tag. This tag is essentially a "type-level natural
>>>>>>>> number". By way of example, here's what I mean:
>>>>>>>>
>>>>>>>> datatype zero = Zero
>>>>>>>> datatype 'n succ = Succ
>>>>>>>>
>>>>>>>> (* example: rose tree *)
>>>>>>>> datatype ('tree, 'list) rose_tree = Node of int * ('list, 'tree) rose_list
>>>>>>>> and ('list, 'tree) rose_list = Nil | Cons of int * ('tree, 'list) rose_list
>>>>>>>>
>>>>>>>> (* example: tree with int list data *)
>>>>>>>> datatype 'list my_list = Nil | Cons of int * 'list my_list
>>>>>>>> and ('tree, 'list) my_tree = Leaf | Node of ('tree, 'list) my_tree * 'list my_list * ('tree, 'list) my_tree
>>>>>>>>
>>>>>>>> As seen, each type is given as many type parameters as is necessary
>>>>>>>> to instantiate its own tag as well as the tags of its "recursive
>>>>>>>> sub-structures". The first type argument is meant for the tag of the
>>>>>>>> recursive type currently being defined.
>>>>>>>>
>>>>>>>> Now, when I use MLton to compile this, the tag types seem to be
>>>>>>>> removed during monomorphization. Thus,
>>>>>>>>
>>>>>>>> (zero, zero succ) rose_tree
>>>>>>>> and
>>>>>>>>
>>>>>>>> (zero succ succ, zero succ succ succ) rose_tree)
>>>>>>>> appear to be the same type in SXML. What are my options here, if
>>>>>>>> I'd like to maintain such a type level distinction? Is XML necessarily the
>>>>>>>> furthest down I can go in the compiler pipeline? I'd greatly appreciate
>>>>>>>> some advice here!
>>>>>>>>
>>>>>>>> Thank you,
>>>>>>>> Arnav.
>>>>>>>> ,
>>>>>>>>
>>>>>>>> To unsubscribe from this group and stop receiving emails from it,
>>>>>>>> send an email to mlt...@ml....
>>>>>>>> _______________________________________________
>>>>>>>> MLton-user mailing list
>>>>>>>> MLt...@li...; mlt...@ml...
>>>>>>>> https://lists.sourceforge.net/lists/listinfo/mlton-user
>>>>>>>>
>>>>>>> To unsubscribe from this group and stop receiving emails from it,
>>>>> send an email to mlt...@ml....
>>>>>
>>>>
>>>>
>>>> --
>>>> -- Yawar Raza
>>>>
>>>>
>>>
>>> --
>>> -- Yawar Raza
>>>
>>> To unsubscribe from this group and stop receiving emails from it, send
>>> an email to mlt...@ml....
>>> _______________________________________________
>>> MLton-user mailing list
>>> MLt...@li...; mlt...@ml...
>>> https://lists.sourceforge.net/lists/listinfo/mlton-user
>>>
>>

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

Re: [MLton-user] Interplay between empty datatypes and monomorphisation

['Yawar R. (R. Student)' v. MLton-u. <mlt...@ml...>]

Gmail didn't add the person I clicked "reply all" to for some reason.
(⁠╯⁠°⁠□⁠°⁠）⁠╯⁠︵⁠ ⁠┻⁠━⁠┻

"I don't know the answer your question, but if you end up finding that
MLton does not meet your needs, you could try using HaMLet instead:
https://github.com/rossberg/hamlet . It's meant to be more amenable to
"hacking" than compilers like MLton are. You could modify the source code
to have more control over type instantiation to match your use case (or
just use it for parsing and do type instantiation in your OCaml code). You
would use this to replace the role of MLton in your current code, so you'd
compile this modified HaMLet (with MLton or any SML compiler) and invoke
the binary from your OCaml code."


> On Friday, July 25, 2025, Arnav Sabharwal <arn...@an...>
> wrote:
>>
>> Hello Prof. Matthew, Yawar,
>>
>> Thank you for your response and advice! Apologies, I miscommunicated
>> earlier: my OCaml "generator" (not generator - generator) takes in an SML
>> type and the user specified target sizes for each involved inductive type
>> and yields an SML term of said type, which meets the size constraints.
>>
>> I was considering the approach of stopping MLton at **some** point since:
>>
>>    1. I was hoping I could get MLton to unique-ify type variables for me
>>    2. MLton could simplify the grammar of type and datatype declarations
>>    for me, making parsing easier (as compared to say, parsing SML from source)
>>
>> Seemingly, the Core-ML IR seems to have these properties? Please correct
>> me if I'm wrong!
>>
>> Thanks,
>> Arnav.
>>
>> On Thu, Jul 24, 2025 at 9:21 PM Matthew Fluet <mat...@gm...>
>> wrote:
>>
>>> Aranav isn’t subscribed, so I needed to moderate/accept the email before
>>> it was sent to the whole list.
>>>
>>> On Thu, Jul 24, 2025 at 8:03 PM 'Yawar Raza (RIT Student)' via
>>> MLton-user <mlt...@ml...> wrote:
>>>
>>>> Nevermind to my first paragraph. I just received the original email.
>>>> Apparently they can get sent to me out of order...
>>>>
>>>> On Thursday, July 24, 2025, Yawar Raza (RIT Student) <ys...@ri...>
>>>> wrote:
>>>>
>>>>> Arnav, I think you might need to use "Reply-All" for the reply to
>>>>> remain on the mailing list, as only Prof. Fluet got your second email (I
>>>>> didn't get it, at least).
>>>>>
>>>>> Anyway, I don't think "stopping the MLton compiler part way through"
>>>>> is the best way to do the sort of thing you're trying to do.
>>>>>
>>>>> Something you _could_ look into is this one family of SML tricks
>>>>> centered around http://mlton.org/Fold, possibly more specifically
>>>>> http://mlton.org/VariableArityPolymorphism. I don't really understand
>>>>> these libraries though, and I'm personally very averse to this sort of code.
>>>>>
>>>>> I don't really get what you're trying to do. Why do you have a
>>>>> generator-generator? Is the generator (output by the generator-generator)
>>>>> in SML itself or does it just output SML? Does it output just datatype
>>>>> declarations or complete programs? I think saying what each level inputs
>>>>> and outputs would be helpful.
>>>>>
>>>>> In general, you should probably end up doing one of the following:
>>>>> - Push arity-polymorphism or similarly un-simple stuff up one
>>>>> generator level, generating different SML source code text for each (rather
>>>>> than trying to extract MLton compiler output).
>>>>> - Give up on perfect type safety relating to arities, and just have
>>>>> the different arities of some things share a single general type.
>>>>> - Use a different language that either has dependent types (e.g.
>>>>> Idris) or has more featureful metaprogramming (e.g. F# with its type
>>>>> providers).
>>>>>
>>>>> But maybe I'm just misunderstanding something. Feel free to ignore
>>>>> those last two paragraph if so, but I hope those two MLton links above were
>>>>> useful to learn exist, at least.
>>>>>
>>>>>
>>>>> On Thursday, July 24, 2025, Matthew Fluet <mat...@gm...>
>>>>> wrote:
>>>>>>
>>>>>> Well, if you just want a somewhat normalized representation of the
>>>>>> types, then you might just use the CoreML representation immediately after
>>>>>> elaboration (`-keep-pass parseAndElaborate`).
>>>>>>
>>>>>> For example:
>>>>>> ```
>>>>>> $ cat z.sml
>>>>>> datatype zero = Zero
>>>>>> datatype 'n succ = Succ
>>>>>>
>>>>>> datatype ('elem, 'index) my_list = Nil | Cons of 'elem * ('elem,
>>>>>> 'index) my_list
>>>>>> val z : ((int, zero) my_list, zero succ) my_list = raise Fail "todo"
>>>>>> $ mlton -keep-pass parseAndElaborate z.sml
>>>>>> $ tail z.parseAndElaborate.post.core-ml
>>>>>> (* deadCode: true *)
>>>>>> (* deadCode: true *)
>>>>>> (* deadCode: false *)
>>>>>> datatype zero_21 = Zero_0
>>>>>> datatype 'a_4547 succ_2 = Succ_0
>>>>>> datatype ('a_4549, 'a_4548) my_list_0 = Nil_0
>>>>>>                                         | Cons_0 of 'a_4549
>>>>>>                                                     * ('a_4549,
>>>>>> 'a_4548) my_list_0
>>>>>> val z_26: ((int32, zero_21) my_list_0, zero_21 succ_2) my_list_0 =
>>>>>>    raise (Fail_0 "todo")
>>>>>> ```
>>>>>>
>>>>>> But, note, you'll still need to see through the uniquification of all
>>>>>> identifiers.
>>>>>>
>>>>>> -Matthew
>>>>>>
>>>>>> On Thu, Jul 24, 2025 at 10:48 AM Arnav Sabharwal <
>>>>>> arn...@an...> wrote:
>>>>>>
>>>>>>> Hello Matthew,
>>>>>>>
>>>>>>> Thank you for your response! My larger goal here is to make a random
>>>>>>> generator for (regular) SML inductive types that allows the user to
>>>>>>> configure "target sizes" for every inductive structure within their type.
>>>>>>> The type labels are meant to be a way for the user and the tool to agree on
>>>>>>> a common language for referring to said inductive types.
>>>>>>>
>>>>>>> For example, say the user wants to generate 2-d lists where the
>>>>>>> outer list has length 3 and each inner list has length 2. Then, they'd
>>>>>>> define their list type like so, building towards their monomorphic "final"
>>>>>>> type:
>>>>>>> ```
>>>>>>> datatype ('elem, 'index) my_list = Nil | Cons of 'elem * ('elem,
>>>>>>> 'index) my_list
>>>>>>> type final = ((int, zero) my_list, zero succ) my_list
>>>>>>> ```
>>>>>>> This way, the user could later provide the lengths [2, 3] and the
>>>>>>> tool would unambiguously be able to generate the type with the
>>>>>>> specified constraints.
>>>>>>>
>>>>>>> Oh, and I'm writing the "random generator"-generator tool in OCaml.
>>>>>>> So, I suppose one way could be to parse out the data-type and type
>>>>>>> declarations from source, while these tags still hang around. But then I'd
>>>>>>> have to "evaluate" type applications to bring them into a normal form, due
>>>>>>> to the lingering type variables...which is why I was considering delaying
>>>>>>> the point at which I "parse into an OCaml representation" as much as
>>>>>>> possible.
>>>>>>>
>>>>>>> Happy to clarify more if necessary, would greatly appreciate your
>>>>>>> advice!
>>>>>>>
>>>>>>> Arnav.
>>>>>>>
>>>>>>> On Thu, Jul 24, 2025 at 8:57 AM Matthew Fluet <
>>>>>>> mat...@gm...> wrote:
>>>>>>>
>>>>>>>> Arnav,
>>>>>>>>
>>>>>>>> Yes, in SXML ("Simply-typed" XML), there is no polymorphism
>>>>>>>> whatsoever (for functions or datatypes) and type parameters that do not
>>>>>>>> contribute to the representation of a datatype will have been eliminated.
>>>>>>>>
>>>>>>>> Actually, the SimplfyTypes (http://mlton.org/XMLSimplifyTypes) XML
>>>>>>>> optimization will have already eliminated these unused type parameters,
>>>>>>>> before monomorphisation.  The motivation for SimplifyTypes is to avoid code
>>>>>>>> duplication by monomorphisation that is unnecessary, due to type parameters
>>>>>>>> that may be present for high-level API reasons, but do not affect the
>>>>>>>> dynamics because they do not influence the data representation.
>>>>>>>>
>>>>>>>> It may be that if you drop SimplifyTypes (compile with `-drop-pass
>>>>>>>> xmlSimplifyTypes`), then monomorphisation will force different "versions"
>>>>>>>> of your tagged datatypes to be separately monmorphised, though with the
>>>>>>>> current heuristics for naming monomorphised variants, you probably won't
>>>>>>>> get any evidence of the `zero` or `succ` type parameters remaining in the
>>>>>>>> SXML program.
>>>>>>>>
>>>>>>>> Could you say a bit more about your goals?  That might help to
>>>>>>>> inform whether there is a better way to accomplish what you are trying to
>>>>>>>> do.
>>>>>>>>
>>>>>>>> -Matthew
>>>>>>>>
>>>>>>>> On Thu, Jul 24, 2025 at 5:24 AM Arnav Sabharwal <
>>>>>>>> arn...@an...> wrote:
>>>>>>>>
>>>>>>>>> Hello,
>>>>>>>>>
>>>>>>>>> I'm trying to tag every instance of a recursive type in a type
>>>>>>>>> definition with a tag. This tag is essentially a "type-level natural
>>>>>>>>> number". By way of example, here's what I mean:
>>>>>>>>>
>>>>>>>>> datatype zero = Zero
>>>>>>>>> datatype 'n succ = Succ
>>>>>>>>>
>>>>>>>>> (* example: rose tree *)
>>>>>>>>> datatype ('tree, 'list) rose_tree = Node of int * ('list, 'tree) rose_list
>>>>>>>>> and ('list, 'tree) rose_list = Nil | Cons of int * ('tree, 'list) rose_list
>>>>>>>>>
>>>>>>>>> (* example: tree with int list data *)
>>>>>>>>> datatype 'list my_list = Nil | Cons of int * 'list my_list
>>>>>>>>> and ('tree, 'list) my_tree = Leaf | Node of ('tree, 'list) my_tree * 'list my_list * ('tree, 'list) my_tree
>>>>>>>>>
>>>>>>>>> As seen, each type is given as many type parameters as is
>>>>>>>>> necessary to instantiate its own tag as well as the tags of its "recursive
>>>>>>>>> sub-structures". The first type argument is meant for the tag of the
>>>>>>>>> recursive type currently being defined.
>>>>>>>>>
>>>>>>>>> Now, when I use MLton to compile this, the tag types seem to be
>>>>>>>>> removed during monomorphization. Thus,
>>>>>>>>>
>>>>>>>>> (zero, zero succ) rose_tree
>>>>>>>>> and
>>>>>>>>>
>>>>>>>>> (zero succ succ, zero succ succ succ) rose_tree)
>>>>>>>>> appear to be the same type in SXML. What are my options here, if
>>>>>>>>> I'd like to maintain such a type level distinction? Is XML necessarily the
>>>>>>>>> furthest down I can go in the compiler pipeline? I'd greatly appreciate
>>>>>>>>> some advice here!
>>>>>>>>>
>>>>>>>>> Thank you,
>>>>>>>>> Arnav.
>>>>>>>>> ,
>>>>>>>>>
>>>>>>>>> To unsubscribe from this group and stop receiving emails from it,
>>>>>>>>> send an email to mlt...@ml....
>>>>>>>>> _______________________________________________
>>>>>>>>> MLton-user mailing list
>>>>>>>>> MLt...@li...; mlt...@ml...
>>>>>>>>> https://lists.sourceforge.net/lists/listinfo/mlton-user
>>>>>>>>>
>>>>>>>> To unsubscribe from this group and stop receiving emails from it,
>>>>>> send an email to mlt...@ml....
>>>>>>
>>>>>
>>>>>
>>>>> --
>>>>> -- Yawar Raza
>>>>>
>>>>>
>>>>
>>>> --
>>>> -- Yawar Raza
>>>>
>>>> To unsubscribe from this group and stop receiving emails from it, send
>>>> an email to mlt...@ml....
>>>> _______________________________________________
>>>> MLton-user mailing list
>>>> MLt...@li...; mlt...@ml...
>>>> https://lists.sourceforge.net/lists/listinfo/mlton-user
>>>>
>>> To unsubscribe from this group and stop receiving emails from it, send
>> an email to mlt...@ml....
>>
>
>
> --
> -- Yawar Raza
>
>

-- 
-- Yawar Raza

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

Re: [MLton-user] Interplay between empty datatypes and monomorphisation

['Yawar R. (R. Student)' v. MLton-u. <mlt...@ml...>]

I don't know the answer your question, but if you end up finding that MLton
does not meet your needs, you could try using HaMLet instead:
https://github.com/rossberg/hamlet . It's meant to be more amenable to
"hacking" than compilers like MLton are. You could modify the source code
to have more control over type instantiation to match your use case (or
just use it for parsing and do type instantiation in your OCaml code). You
would use this to replace the role of MLton in your current code, so you'd
compile this modified HaMLet (with MLton or any SML compiler) and invoke
the binary from your OCaml code.

On Friday, July 25, 2025, Arnav Sabharwal <arn...@an...> wrote:
>
> Hello Prof. Matthew, Yawar,
>
> Thank you for your response and advice! Apologies, I miscommunicated
> earlier: my OCaml "generator" (not generator - generator) takes in an SML
> type and the user specified target sizes for each involved inductive type
> and yields an SML term of said type, which meets the size constraints.
>
> I was considering the approach of stopping MLton at **some** point since:
>
>    1. I was hoping I could get MLton to unique-ify type variables for me
>    2. MLton could simplify the grammar of type and datatype declarations
>    for me, making parsing easier (as compared to say, parsing SML from source)
>
> Seemingly, the Core-ML IR seems to have these properties? Please correct
> me if I'm wrong!
>
> Thanks,
> Arnav.
>
> On Thu, Jul 24, 2025 at 9:21 PM Matthew Fluet <mat...@gm...>
> wrote:
>
>> Aranav isn’t subscribed, so I needed to moderate/accept the email before
>> it was sent to the whole list.
>>
>> On Thu, Jul 24, 2025 at 8:03 PM 'Yawar Raza (RIT Student)' via MLton-user
>> <mlt...@ml...> wrote:
>>
>>> Nevermind to my first paragraph. I just received the original email.
>>> Apparently they can get sent to me out of order...
>>>
>>> On Thursday, July 24, 2025, Yawar Raza (RIT Student) <ys...@ri...>
>>> wrote:
>>>
>>>> Arnav, I think you might need to use "Reply-All" for the reply to
>>>> remain on the mailing list, as only Prof. Fluet got your second email (I
>>>> didn't get it, at least).
>>>>
>>>> Anyway, I don't think "stopping the MLton compiler part way through" is
>>>> the best way to do the sort of thing you're trying to do.
>>>>
>>>> Something you _could_ look into is this one family of SML tricks
>>>> centered around http://mlton.org/Fold, possibly more specifically
>>>> http://mlton.org/VariableArityPolymorphism. I don't really understand
>>>> these libraries though, and I'm personally very averse to this sort of code.
>>>>
>>>> I don't really get what you're trying to do. Why do you have a
>>>> generator-generator? Is the generator (output by the generator-generator)
>>>> in SML itself or does it just output SML? Does it output just datatype
>>>> declarations or complete programs? I think saying what each level inputs
>>>> and outputs would be helpful.
>>>>
>>>> In general, you should probably end up doing one of the following:
>>>> - Push arity-polymorphism or similarly un-simple stuff up one generator
>>>> level, generating different SML source code text for each (rather than
>>>> trying to extract MLton compiler output).
>>>> - Give up on perfect type safety relating to arities, and just have the
>>>> different arities of some things share a single general type.
>>>> - Use a different language that either has dependent types (e.g. Idris)
>>>> or has more featureful metaprogramming (e.g. F# with its type providers).
>>>>
>>>> But maybe I'm just misunderstanding something. Feel free to ignore
>>>> those last two paragraph if so, but I hope those two MLton links above were
>>>> useful to learn exist, at least.
>>>>
>>>>
>>>> On Thursday, July 24, 2025, Matthew Fluet <mat...@gm...>
>>>> wrote:
>>>>>
>>>>> Well, if you just want a somewhat normalized representation of the
>>>>> types, then you might just use the CoreML representation immediately after
>>>>> elaboration (`-keep-pass parseAndElaborate`).
>>>>>
>>>>> For example:
>>>>> ```
>>>>> $ cat z.sml
>>>>> datatype zero = Zero
>>>>> datatype 'n succ = Succ
>>>>>
>>>>> datatype ('elem, 'index) my_list = Nil | Cons of 'elem * ('elem,
>>>>> 'index) my_list
>>>>> val z : ((int, zero) my_list, zero succ) my_list = raise Fail "todo"
>>>>> $ mlton -keep-pass parseAndElaborate z.sml
>>>>> $ tail z.parseAndElaborate.post.core-ml
>>>>> (* deadCode: true *)
>>>>> (* deadCode: true *)
>>>>> (* deadCode: false *)
>>>>> datatype zero_21 = Zero_0
>>>>> datatype 'a_4547 succ_2 = Succ_0
>>>>> datatype ('a_4549, 'a_4548) my_list_0 = Nil_0
>>>>>                                         | Cons_0 of 'a_4549
>>>>>                                                     * ('a_4549,
>>>>> 'a_4548) my_list_0
>>>>> val z_26: ((int32, zero_21) my_list_0, zero_21 succ_2) my_list_0 =
>>>>>    raise (Fail_0 "todo")
>>>>> ```
>>>>>
>>>>> But, note, you'll still need to see through the uniquification of all
>>>>> identifiers.
>>>>>
>>>>> -Matthew
>>>>>
>>>>> On Thu, Jul 24, 2025 at 10:48 AM Arnav Sabharwal <
>>>>> arn...@an...> wrote:
>>>>>
>>>>>> Hello Matthew,
>>>>>>
>>>>>> Thank you for your response! My larger goal here is to make a random
>>>>>> generator for (regular) SML inductive types that allows the user to
>>>>>> configure "target sizes" for every inductive structure within their type.
>>>>>> The type labels are meant to be a way for the user and the tool to agree on
>>>>>> a common language for referring to said inductive types.
>>>>>>
>>>>>> For example, say the user wants to generate 2-d lists where the outer
>>>>>> list has length 3 and each inner list has length 2. Then, they'd define
>>>>>> their list type like so, building towards their monomorphic "final" type:
>>>>>> ```
>>>>>> datatype ('elem, 'index) my_list = Nil | Cons of 'elem * ('elem,
>>>>>> 'index) my_list
>>>>>> type final = ((int, zero) my_list, zero succ) my_list
>>>>>> ```
>>>>>> This way, the user could later provide the lengths [2, 3] and the
>>>>>> tool would unambiguously be able to generate the type with the
>>>>>> specified constraints.
>>>>>>
>>>>>> Oh, and I'm writing the "random generator"-generator tool in OCaml.
>>>>>> So, I suppose one way could be to parse out the data-type and type
>>>>>> declarations from source, while these tags still hang around. But then I'd
>>>>>> have to "evaluate" type applications to bring them into a normal form, due
>>>>>> to the lingering type variables...which is why I was considering delaying
>>>>>> the point at which I "parse into an OCaml representation" as much as
>>>>>> possible.
>>>>>>
>>>>>> Happy to clarify more if necessary, would greatly appreciate your
>>>>>> advice!
>>>>>>
>>>>>> Arnav.
>>>>>>
>>>>>> On Thu, Jul 24, 2025 at 8:57 AM Matthew Fluet <
>>>>>> mat...@gm...> wrote:
>>>>>>
>>>>>>> Arnav,
>>>>>>>
>>>>>>> Yes, in SXML ("Simply-typed" XML), there is no polymorphism
>>>>>>> whatsoever (for functions or datatypes) and type parameters that do not
>>>>>>> contribute to the representation of a datatype will have been eliminated.
>>>>>>>
>>>>>>> Actually, the SimplfyTypes (http://mlton.org/XMLSimplifyTypes) XML
>>>>>>> optimization will have already eliminated these unused type parameters,
>>>>>>> before monomorphisation.  The motivation for SimplifyTypes is to avoid code
>>>>>>> duplication by monomorphisation that is unnecessary, due to type parameters
>>>>>>> that may be present for high-level API reasons, but do not affect the
>>>>>>> dynamics because they do not influence the data representation.
>>>>>>>
>>>>>>> It may be that if you drop SimplifyTypes (compile with `-drop-pass
>>>>>>> xmlSimplifyTypes`), then monomorphisation will force different "versions"
>>>>>>> of your tagged datatypes to be separately monmorphised, though with the
>>>>>>> current heuristics for naming monomorphised variants, you probably won't
>>>>>>> get any evidence of the `zero` or `succ` type parameters remaining in the
>>>>>>> SXML program.
>>>>>>>
>>>>>>> Could you say a bit more about your goals?  That might help to
>>>>>>> inform whether there is a better way to accomplish what you are trying to
>>>>>>> do.
>>>>>>>
>>>>>>> -Matthew
>>>>>>>
>>>>>>> On Thu, Jul 24, 2025 at 5:24 AM Arnav Sabharwal <
>>>>>>> arn...@an...> wrote:
>>>>>>>
>>>>>>>> Hello,
>>>>>>>>
>>>>>>>> I'm trying to tag every instance of a recursive type in a type
>>>>>>>> definition with a tag. This tag is essentially a "type-level natural
>>>>>>>> number". By way of example, here's what I mean:
>>>>>>>>
>>>>>>>> datatype zero = Zero
>>>>>>>> datatype 'n succ = Succ
>>>>>>>>
>>>>>>>> (* example: rose tree *)
>>>>>>>> datatype ('tree, 'list) rose_tree = Node of int * ('list, 'tree) rose_list
>>>>>>>> and ('list, 'tree) rose_list = Nil | Cons of int * ('tree, 'list) rose_list
>>>>>>>>
>>>>>>>> (* example: tree with int list data *)
>>>>>>>> datatype 'list my_list = Nil | Cons of int * 'list my_list
>>>>>>>> and ('tree, 'list) my_tree = Leaf | Node of ('tree, 'list) my_tree * 'list my_list * ('tree, 'list) my_tree
>>>>>>>>
>>>>>>>> As seen, each type is given as many type parameters as is necessary
>>>>>>>> to instantiate its own tag as well as the tags of its "recursive
>>>>>>>> sub-structures". The first type argument is meant for the tag of the
>>>>>>>> recursive type currently being defined.
>>>>>>>>
>>>>>>>> Now, when I use MLton to compile this, the tag types seem to be
>>>>>>>> removed during monomorphization. Thus,
>>>>>>>>
>>>>>>>> (zero, zero succ) rose_tree
>>>>>>>> and
>>>>>>>>
>>>>>>>> (zero succ succ, zero succ succ succ) rose_tree)
>>>>>>>> appear to be the same type in SXML. What are my options here, if
>>>>>>>> I'd like to maintain such a type level distinction? Is XML necessarily the
>>>>>>>> furthest down I can go in the compiler pipeline? I'd greatly appreciate
>>>>>>>> some advice here!
>>>>>>>>
>>>>>>>> Thank you,
>>>>>>>> Arnav.
>>>>>>>> ,
>>>>>>>>
>>>>>>>> To unsubscribe from this group and stop receiving emails from it,
>>>>>>>> send an email to mlt...@ml....
>>>>>>>> _______________________________________________
>>>>>>>> MLton-user mailing list
>>>>>>>> MLt...@li...; mlt...@ml...
>>>>>>>> https://lists.sourceforge.net/lists/listinfo/mlton-user
>>>>>>>>
>>>>>>> To unsubscribe from this group and stop receiving emails from it,
>>>>> send an email to mlt...@ml....
>>>>>
>>>>
>>>>
>>>> --
>>>> -- Yawar Raza
>>>>
>>>>
>>>
>>> --
>>> -- Yawar Raza
>>>
>>> To unsubscribe from this group and stop receiving emails from it, send
>>> an email to mlt...@ml....
>>> _______________________________________________
>>> MLton-user mailing list
>>> MLt...@li...; mlt...@ml...
>>> https://lists.sourceforge.net/lists/listinfo/mlton-user
>>>
>> To unsubscribe from this group and stop receiving emails from it, send an
> email to mlt...@ml....
>


-- 
-- Yawar Raza

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

Re: [MLton-user] Interplay between empty datatypes and monomorphisation

[Arnav S. <arn...@an...>]

Hello Prof. Matthew, Yawar,

Thank you for your response and advice! Apologies, I miscommunicated
earlier: my OCaml "generator" (not generator - generator) takes in an SML
type and the user specified target sizes for each involved inductive type
and yields an SML term of said type, which meets the size constraints.

I was considering the approach of stopping MLton at **some** point since:

   1. I was hoping I could get MLton to unique-ify type variables for me
   2. MLton could simplify the grammar of type and datatype declarations
   for me, making parsing easier (as compared to say, parsing SML from source)

Seemingly, the Core-ML IR seems to have these properties? Please correct
me if I'm wrong!

Thanks,
Arnav.

On Thu, Jul 24, 2025 at 9:21 PM Matthew Fluet <mat...@gm...>
wrote:

> Aranav isn’t subscribed, so I needed to moderate/accept the email before
> it was sent to the whole list.
>
> On Thu, Jul 24, 2025 at 8:03 PM 'Yawar Raza (RIT Student)' via MLton-user <
> mlt...@ml...> wrote:
>
>> Nevermind to my first paragraph. I just received the original email.
>> Apparently they can get sent to me out of order...
>>
>> On Thursday, July 24, 2025, Yawar Raza (RIT Student) <ys...@ri...>
>> wrote:
>>
>>> Arnav, I think you might need to use "Reply-All" for the reply to remain
>>> on the mailing list, as only Prof. Fluet got your second email (I didn't
>>> get it, at least).
>>>
>>> Anyway, I don't think "stopping the MLton compiler part way through" is
>>> the best way to do the sort of thing you're trying to do.
>>>
>>> Something you _could_ look into is this one family of SML tricks
>>> centered around http://mlton.org/Fold, possibly more specifically
>>> http://mlton.org/VariableArityPolymorphism. I don't really understand
>>> these libraries though, and I'm personally very averse to this sort of code.
>>>
>>> I don't really get what you're trying to do. Why do you have a
>>> generator-generator? Is the generator (output by the generator-generator)
>>> in SML itself or does it just output SML? Does it output just datatype
>>> declarations or complete programs? I think saying what each level inputs
>>> and outputs would be helpful.
>>>
>>> In general, you should probably end up doing one of the following:
>>> - Push arity-polymorphism or similarly un-simple stuff up one generator
>>> level, generating different SML source code text for each (rather than
>>> trying to extract MLton compiler output).
>>> - Give up on perfect type safety relating to arities, and just have the
>>> different arities of some things share a single general type.
>>> - Use a different language that either has dependent types (e.g. Idris)
>>> or has more featureful metaprogramming (e.g. F# with its type providers).
>>>
>>> But maybe I'm just misunderstanding something. Feel free to ignore those
>>> last two paragraph if so, but I hope those two MLton links above were
>>> useful to learn exist, at least.
>>>
>>>
>>> On Thursday, July 24, 2025, Matthew Fluet <mat...@gm...>
>>> wrote:
>>>>
>>>> Well, if you just want a somewhat normalized representation of the
>>>> types, then you might just use the CoreML representation immediately after
>>>> elaboration (`-keep-pass parseAndElaborate`).
>>>>
>>>> For example:
>>>> ```
>>>> $ cat z.sml
>>>> datatype zero = Zero
>>>> datatype 'n succ = Succ
>>>>
>>>> datatype ('elem, 'index) my_list = Nil | Cons of 'elem * ('elem,
>>>> 'index) my_list
>>>> val z : ((int, zero) my_list, zero succ) my_list = raise Fail "todo"
>>>> $ mlton -keep-pass parseAndElaborate z.sml
>>>> $ tail z.parseAndElaborate.post.core-ml
>>>> (* deadCode: true *)
>>>> (* deadCode: true *)
>>>> (* deadCode: false *)
>>>> datatype zero_21 = Zero_0
>>>> datatype 'a_4547 succ_2 = Succ_0
>>>> datatype ('a_4549, 'a_4548) my_list_0 = Nil_0
>>>>                                         | Cons_0 of 'a_4549
>>>>                                                     * ('a_4549,
>>>> 'a_4548) my_list_0
>>>> val z_26: ((int32, zero_21) my_list_0, zero_21 succ_2) my_list_0 =
>>>>    raise (Fail_0 "todo")
>>>> ```
>>>>
>>>> But, note, you'll still need to see through the uniquification of all
>>>> identifiers.
>>>>
>>>> -Matthew
>>>>
>>>> On Thu, Jul 24, 2025 at 10:48 AM Arnav Sabharwal <
>>>> arn...@an...> wrote:
>>>>
>>>>> Hello Matthew,
>>>>>
>>>>> Thank you for your response! My larger goal here is to make a random
>>>>> generator for (regular) SML inductive types that allows the user to
>>>>> configure "target sizes" for every inductive structure within their type.
>>>>> The type labels are meant to be a way for the user and the tool to agree on
>>>>> a common language for referring to said inductive types.
>>>>>
>>>>> For example, say the user wants to generate 2-d lists where the outer
>>>>> list has length 3 and each inner list has length 2. Then, they'd define
>>>>> their list type like so, building towards their monomorphic "final" type:
>>>>> ```
>>>>> datatype ('elem, 'index) my_list = Nil | Cons of 'elem * ('elem,
>>>>> 'index) my_list
>>>>> type final = ((int, zero) my_list, zero succ) my_list
>>>>> ```
>>>>> This way, the user could later provide the lengths [2, 3] and the tool
>>>>> would unambiguously be able to generate the type with the
>>>>> specified constraints.
>>>>>
>>>>> Oh, and I'm writing the "random generator"-generator tool in OCaml.
>>>>> So, I suppose one way could be to parse out the data-type and type
>>>>> declarations from source, while these tags still hang around. But then I'd
>>>>> have to "evaluate" type applications to bring them into a normal form, due
>>>>> to the lingering type variables...which is why I was considering delaying
>>>>> the point at which I "parse into an OCaml representation" as much as
>>>>> possible.
>>>>>
>>>>> Happy to clarify more if necessary, would greatly appreciate your
>>>>> advice!
>>>>>
>>>>> Arnav.
>>>>>
>>>>> On Thu, Jul 24, 2025 at 8:57 AM Matthew Fluet <mat...@gm...>
>>>>> wrote:
>>>>>
>>>>>> Arnav,
>>>>>>
>>>>>> Yes, in SXML ("Simply-typed" XML), there is no polymorphism
>>>>>> whatsoever (for functions or datatypes) and type parameters that do not
>>>>>> contribute to the representation of a datatype will have been eliminated.
>>>>>>
>>>>>> Actually, the SimplfyTypes (http://mlton.org/XMLSimplifyTypes) XML
>>>>>> optimization will have already eliminated these unused type parameters,
>>>>>> before monomorphisation.  The motivation for SimplifyTypes is to avoid code
>>>>>> duplication by monomorphisation that is unnecessary, due to type parameters
>>>>>> that may be present for high-level API reasons, but do not affect the
>>>>>> dynamics because they do not influence the data representation.
>>>>>>
>>>>>> It may be that if you drop SimplifyTypes (compile with `-drop-pass
>>>>>> xmlSimplifyTypes`), then monomorphisation will force different "versions"
>>>>>> of your tagged datatypes to be separately monmorphised, though with the
>>>>>> current heuristics for naming monomorphised variants, you probably won't
>>>>>> get any evidence of the `zero` or `succ` type parameters remaining in the
>>>>>> SXML program.
>>>>>>
>>>>>> Could you say a bit more about your goals?  That might help to inform
>>>>>> whether there is a better way to accomplish what you are trying to do.
>>>>>>
>>>>>> -Matthew
>>>>>>
>>>>>> On Thu, Jul 24, 2025 at 5:24 AM Arnav Sabharwal <
>>>>>> arn...@an...> wrote:
>>>>>>
>>>>>>> Hello,
>>>>>>>
>>>>>>> I'm trying to tag every instance of a recursive type in a type
>>>>>>> definition with a tag. This tag is essentially a "type-level natural
>>>>>>> number". By way of example, here's what I mean:
>>>>>>>
>>>>>>> datatype zero = Zero
>>>>>>> datatype 'n succ = Succ
>>>>>>>
>>>>>>> (* example: rose tree *)
>>>>>>> datatype ('tree, 'list) rose_tree = Node of int * ('list, 'tree) rose_list
>>>>>>> and ('list, 'tree) rose_list = Nil | Cons of int * ('tree, 'list) rose_list
>>>>>>>
>>>>>>> (* example: tree with int list data *)
>>>>>>> datatype 'list my_list = Nil | Cons of int * 'list my_list
>>>>>>> and ('tree, 'list) my_tree = Leaf | Node of ('tree, 'list) my_tree * 'list my_list * ('tree, 'list) my_tree
>>>>>>>
>>>>>>> As seen, each type is given as many type parameters as is necessary
>>>>>>> to instantiate its own tag as well as the tags of its "recursive
>>>>>>> sub-structures". The first type argument is meant for the tag of the
>>>>>>> recursive type currently being defined.
>>>>>>>
>>>>>>> Now, when I use MLton to compile this, the tag types seem to be
>>>>>>> removed during monomorphization. Thus,
>>>>>>>
>>>>>>> (zero, zero succ) rose_tree
>>>>>>> and
>>>>>>>
>>>>>>> (zero succ succ, zero succ succ succ) rose_tree)
>>>>>>> appear to be the same type in SXML. What are my options here, if I'd
>>>>>>> like to maintain such a type level distinction? Is XML necessarily the
>>>>>>> furthest down I can go in the compiler pipeline? I'd greatly appreciate
>>>>>>> some advice here!
>>>>>>>
>>>>>>> Thank you,
>>>>>>> Arnav.
>>>>>>> ,
>>>>>>>
>>>>>>> To unsubscribe from this group and stop receiving emails from it,
>>>>>>> send an email to mlt...@ml....
>>>>>>> _______________________________________________
>>>>>>> MLton-user mailing list
>>>>>>> MLt...@li...; mlt...@ml...
>>>>>>> https://lists.sourceforge.net/lists/listinfo/mlton-user
>>>>>>>
>>>>>> To unsubscribe from this group and stop receiving emails from it,
>>>> send an email to mlt...@ml....
>>>>
>>>
>>>
>>> --
>>> -- Yawar Raza
>>>
>>>
>>
>> --
>> -- Yawar Raza
>>
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to mlt...@ml....
>> _______________________________________________
>> MLton-user mailing list
>> MLt...@li...; mlt...@ml...
>> https://lists.sourceforge.net/lists/listinfo/mlton-user
>>
>

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

Re: [MLton-user] Interplay between empty datatypes and monomorphisation

[Matthew F. <mat...@gm...>]

Aranav isn’t subscribed, so I needed to moderate/accept the email before it
was sent to the whole list.

On Thu, Jul 24, 2025 at 8:03 PM 'Yawar Raza (RIT Student)' via MLton-user <
mlt...@ml...> wrote:

> Nevermind to my first paragraph. I just received the original email.
> Apparently they can get sent to me out of order...
>
> On Thursday, July 24, 2025, Yawar Raza (RIT Student) <ys...@ri...>
> wrote:
>
>> Arnav, I think you might need to use "Reply-All" for the reply to remain
>> on the mailing list, as only Prof. Fluet got your second email (I didn't
>> get it, at least).
>>
>> Anyway, I don't think "stopping the MLton compiler part way through" is
>> the best way to do the sort of thing you're trying to do.
>>
>> Something you _could_ look into is this one family of SML tricks centered
>> around http://mlton.org/Fold, possibly more specifically
>> http://mlton.org/VariableArityPolymorphism. I don't really understand
>> these libraries though, and I'm personally very averse to this sort of code.
>>
>> I don't really get what you're trying to do. Why do you have a
>> generator-generator? Is the generator (output by the generator-generator)
>> in SML itself or does it just output SML? Does it output just datatype
>> declarations or complete programs? I think saying what each level inputs
>> and outputs would be helpful.
>>
>> In general, you should probably end up doing one of the following:
>> - Push arity-polymorphism or similarly un-simple stuff up one generator
>> level, generating different SML source code text for each (rather than
>> trying to extract MLton compiler output).
>> - Give up on perfect type safety relating to arities, and just have the
>> different arities of some things share a single general type.
>> - Use a different language that either has dependent types (e.g. Idris)
>> or has more featureful metaprogramming (e.g. F# with its type providers).
>>
>> But maybe I'm just misunderstanding something. Feel free to ignore those
>> last two paragraph if so, but I hope those two MLton links above were
>> useful to learn exist, at least.
>>
>>
>> On Thursday, July 24, 2025, Matthew Fluet <mat...@gm...>
>> wrote:
>>>
>>> Well, if you just want a somewhat normalized representation of the
>>> types, then you might just use the CoreML representation immediately after
>>> elaboration (`-keep-pass parseAndElaborate`).
>>>
>>> For example:
>>> ```
>>> $ cat z.sml
>>> datatype zero = Zero
>>> datatype 'n succ = Succ
>>>
>>> datatype ('elem, 'index) my_list = Nil | Cons of 'elem * ('elem, 'index)
>>> my_list
>>> val z : ((int, zero) my_list, zero succ) my_list = raise Fail "todo"
>>> $ mlton -keep-pass parseAndElaborate z.sml
>>> $ tail z.parseAndElaborate.post.core-ml
>>> (* deadCode: true *)
>>> (* deadCode: true *)
>>> (* deadCode: false *)
>>> datatype zero_21 = Zero_0
>>> datatype 'a_4547 succ_2 = Succ_0
>>> datatype ('a_4549, 'a_4548) my_list_0 = Nil_0
>>>                                         | Cons_0 of 'a_4549
>>>                                                     * ('a_4549, 'a_4548)
>>> my_list_0
>>> val z_26: ((int32, zero_21) my_list_0, zero_21 succ_2) my_list_0 =
>>>    raise (Fail_0 "todo")
>>> ```
>>>
>>> But, note, you'll still need to see through the uniquification of all
>>> identifiers.
>>>
>>> -Matthew
>>>
>>> On Thu, Jul 24, 2025 at 10:48 AM Arnav Sabharwal <
>>> arn...@an...> wrote:
>>>
>>>> Hello Matthew,
>>>>
>>>> Thank you for your response! My larger goal here is to make a random
>>>> generator for (regular) SML inductive types that allows the user to
>>>> configure "target sizes" for every inductive structure within their type.
>>>> The type labels are meant to be a way for the user and the tool to agree on
>>>> a common language for referring to said inductive types.
>>>>
>>>> For example, say the user wants to generate 2-d lists where the outer
>>>> list has length 3 and each inner list has length 2. Then, they'd define
>>>> their list type like so, building towards their monomorphic "final" type:
>>>> ```
>>>> datatype ('elem, 'index) my_list = Nil | Cons of 'elem * ('elem,
>>>> 'index) my_list
>>>> type final = ((int, zero) my_list, zero succ) my_list
>>>> ```
>>>> This way, the user could later provide the lengths [2, 3] and the tool
>>>> would unambiguously be able to generate the type with the
>>>> specified constraints.
>>>>
>>>> Oh, and I'm writing the "random generator"-generator tool in OCaml. So,
>>>> I suppose one way could be to parse out the data-type and type declarations
>>>> from source, while these tags still hang around. But then I'd have to
>>>> "evaluate" type applications to bring them into a normal form, due to the
>>>> lingering type variables...which is why I was considering delaying the
>>>> point at which I "parse into an OCaml representation" as much as possible.
>>>>
>>>> Happy to clarify more if necessary, would greatly appreciate your
>>>> advice!
>>>>
>>>> Arnav.
>>>>
>>>> On Thu, Jul 24, 2025 at 8:57 AM Matthew Fluet <mat...@gm...>
>>>> wrote:
>>>>
>>>>> Arnav,
>>>>>
>>>>> Yes, in SXML ("Simply-typed" XML), there is no polymorphism whatsoever
>>>>> (for functions or datatypes) and type parameters that do not contribute to
>>>>> the representation of a datatype will have been eliminated.
>>>>>
>>>>> Actually, the SimplfyTypes (http://mlton.org/XMLSimplifyTypes) XML
>>>>> optimization will have already eliminated these unused type parameters,
>>>>> before monomorphisation.  The motivation for SimplifyTypes is to avoid code
>>>>> duplication by monomorphisation that is unnecessary, due to type parameters
>>>>> that may be present for high-level API reasons, but do not affect the
>>>>> dynamics because they do not influence the data representation.
>>>>>
>>>>> It may be that if you drop SimplifyTypes (compile with `-drop-pass
>>>>> xmlSimplifyTypes`), then monomorphisation will force different "versions"
>>>>> of your tagged datatypes to be separately monmorphised, though with the
>>>>> current heuristics for naming monomorphised variants, you probably won't
>>>>> get any evidence of the `zero` or `succ` type parameters remaining in the
>>>>> SXML program.
>>>>>
>>>>> Could you say a bit more about your goals?  That might help to inform
>>>>> whether there is a better way to accomplish what you are trying to do.
>>>>>
>>>>> -Matthew
>>>>>
>>>>> On Thu, Jul 24, 2025 at 5:24 AM Arnav Sabharwal <
>>>>> arn...@an...> wrote:
>>>>>
>>>>>> Hello,
>>>>>>
>>>>>> I'm trying to tag every instance of a recursive type in a type
>>>>>> definition with a tag. This tag is essentially a "type-level natural
>>>>>> number". By way of example, here's what I mean:
>>>>>>
>>>>>> datatype zero = Zero
>>>>>> datatype 'n succ = Succ
>>>>>>
>>>>>> (* example: rose tree *)
>>>>>> datatype ('tree, 'list) rose_tree = Node of int * ('list, 'tree) rose_list
>>>>>> and ('list, 'tree) rose_list = Nil | Cons of int * ('tree, 'list) rose_list
>>>>>>
>>>>>> (* example: tree with int list data *)
>>>>>> datatype 'list my_list = Nil | Cons of int * 'list my_list
>>>>>> and ('tree, 'list) my_tree = Leaf | Node of ('tree, 'list) my_tree * 'list my_list * ('tree, 'list) my_tree
>>>>>>
>>>>>> As seen, each type is given as many type parameters as is necessary
>>>>>> to instantiate its own tag as well as the tags of its "recursive
>>>>>> sub-structures". The first type argument is meant for the tag of the
>>>>>> recursive type currently being defined.
>>>>>>
>>>>>> Now, when I use MLton to compile this, the tag types seem to be
>>>>>> removed during monomorphization. Thus,
>>>>>>
>>>>>> (zero, zero succ) rose_tree
>>>>>> and
>>>>>>
>>>>>> (zero succ succ, zero succ succ succ) rose_tree)
>>>>>> appear to be the same type in SXML. What are my options here, if I'd
>>>>>> like to maintain such a type level distinction? Is XML necessarily the
>>>>>> furthest down I can go in the compiler pipeline? I'd greatly appreciate
>>>>>> some advice here!
>>>>>>
>>>>>> Thank you,
>>>>>> Arnav.
>>>>>> ,
>>>>>>
>>>>>> To unsubscribe from this group and stop receiving emails from it,
>>>>>> send an email to mlt...@ml....
>>>>>> _______________________________________________
>>>>>> MLton-user mailing list
>>>>>> MLt...@li...; mlt...@ml...
>>>>>> https://lists.sourceforge.net/lists/listinfo/mlton-user
>>>>>>
>>>>> To unsubscribe from this group and stop receiving emails from it, send
>>> an email to mlt...@ml....
>>>
>>
>>
>> --
>> -- Yawar Raza
>>
>>
>
> --
> -- Yawar Raza
>
> To unsubscribe from this group and stop receiving emails from it, send an
> email to mlt...@ml....
> _______________________________________________
> MLton-user mailing list
> MLt...@li...; mlt...@ml...
> https://lists.sourceforge.net/lists/listinfo/mlton-user
>

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

Re: [MLton-user] Interplay between empty datatypes and monomorphisation

['Yawar R. (R. Student)' v. MLton-u. <mlt...@ml...>]

Nevermind to my first paragraph. I just received the original email.
Apparently they can get sent to me out of order...

On Thursday, July 24, 2025, Yawar Raza (RIT Student) <ys...@ri...>
wrote:

> Arnav, I think you might need to use "Reply-All" for the reply to remain
> on the mailing list, as only Prof. Fluet got your second email (I didn't
> get it, at least).
>
> Anyway, I don't think "stopping the MLton compiler part way through" is
> the best way to do the sort of thing you're trying to do.
>
> Something you _could_ look into is this one family of SML tricks centered
> around http://mlton.org/Fold, possibly more specifically http://mlton.org/
> VariableArityPolymorphism. I don't really understand these libraries
> though, and I'm personally very averse to this sort of code.
>
> I don't really get what you're trying to do. Why do you have a
> generator-generator? Is the generator (output by the generator-generator)
> in SML itself or does it just output SML? Does it output just datatype
> declarations or complete programs? I think saying what each level inputs
> and outputs would be helpful.
>
> In general, you should probably end up doing one of the following:
> - Push arity-polymorphism or similarly un-simple stuff up one generator
> level, generating different SML source code text for each (rather than
> trying to extract MLton compiler output).
> - Give up on perfect type safety relating to arities, and just have the
> different arities of some things share a single general type.
> - Use a different language that either has dependent types (e.g. Idris) or
> has more featureful metaprogramming (e.g. F# with its type providers).
>
> But maybe I'm just misunderstanding something. Feel free to ignore those
> last two paragraph if so, but I hope those two MLton links above were
> useful to learn exist, at least.
>
>
> On Thursday, July 24, 2025, Matthew Fluet <mat...@gm...> wrote:
>>
>> Well, if you just want a somewhat normalized representation of the types,
>> then you might just use the CoreML representation immediately after
>> elaboration (`-keep-pass parseAndElaborate`).
>>
>> For example:
>> ```
>> $ cat z.sml
>> datatype zero = Zero
>> datatype 'n succ = Succ
>>
>> datatype ('elem, 'index) my_list = Nil | Cons of 'elem * ('elem, 'index)
>> my_list
>> val z : ((int, zero) my_list, zero succ) my_list = raise Fail "todo"
>> $ mlton -keep-pass parseAndElaborate z.sml
>> $ tail z.parseAndElaborate.post.core-ml
>> (* deadCode: true *)
>> (* deadCode: true *)
>> (* deadCode: false *)
>> datatype zero_21 = Zero_0
>> datatype 'a_4547 succ_2 = Succ_0
>> datatype ('a_4549, 'a_4548) my_list_0 = Nil_0
>>                                         | Cons_0 of 'a_4549
>>                                                     * ('a_4549, 'a_4548)
>> my_list_0
>> val z_26: ((int32, zero_21) my_list_0, zero_21 succ_2) my_list_0 =
>>    raise (Fail_0 "todo")
>> ```
>>
>> But, note, you'll still need to see through the uniquification of all
>> identifiers.
>>
>> -Matthew
>>
>> On Thu, Jul 24, 2025 at 10:48 AM Arnav Sabharwal <arn...@an...>
>> wrote:
>>
>>> Hello Matthew,
>>>
>>> Thank you for your response! My larger goal here is to make a random
>>> generator for (regular) SML inductive types that allows the user to
>>> configure "target sizes" for every inductive structure within their type.
>>> The type labels are meant to be a way for the user and the tool to agree on
>>> a common language for referring to said inductive types.
>>>
>>> For example, say the user wants to generate 2-d lists where the outer
>>> list has length 3 and each inner list has length 2. Then, they'd define
>>> their list type like so, building towards their monomorphic "final" type:
>>> ```
>>> datatype ('elem, 'index) my_list = Nil | Cons of 'elem * ('elem, 'index)
>>> my_list
>>> type final = ((int, zero) my_list, zero succ) my_list
>>> ```
>>> This way, the user could later provide the lengths [2, 3] and the tool
>>> would unambiguously be able to generate the type with the
>>> specified constraints.
>>>
>>> Oh, and I'm writing the "random generator"-generator tool in OCaml. So,
>>> I suppose one way could be to parse out the data-type and type declarations
>>> from source, while these tags still hang around. But then I'd have to
>>> "evaluate" type applications to bring them into a normal form, due to the
>>> lingering type variables...which is why I was considering delaying the
>>> point at which I "parse into an OCaml representation" as much as possible.
>>>
>>> Happy to clarify more if necessary, would greatly appreciate your advice!
>>>
>>> Arnav.
>>>
>>> On Thu, Jul 24, 2025 at 8:57 AM Matthew Fluet <mat...@gm...>
>>> wrote:
>>>
>>>> Arnav,
>>>>
>>>> Yes, in SXML ("Simply-typed" XML), there is no polymorphism whatsoever
>>>> (for functions or datatypes) and type parameters that do not contribute to
>>>> the representation of a datatype will have been eliminated.
>>>>
>>>> Actually, the SimplfyTypes (http://mlton.org/XMLSimplifyTypes) XML
>>>> optimization will have already eliminated these unused type parameters,
>>>> before monomorphisation.  The motivation for SimplifyTypes is to avoid code
>>>> duplication by monomorphisation that is unnecessary, due to type parameters
>>>> that may be present for high-level API reasons, but do not affect the
>>>> dynamics because they do not influence the data representation.
>>>>
>>>> It may be that if you drop SimplifyTypes (compile with `-drop-pass
>>>> xmlSimplifyTypes`), then monomorphisation will force different "versions"
>>>> of your tagged datatypes to be separately monmorphised, though with the
>>>> current heuristics for naming monomorphised variants, you probably won't
>>>> get any evidence of the `zero` or `succ` type parameters remaining in the
>>>> SXML program.
>>>>
>>>> Could you say a bit more about your goals?  That might help to inform
>>>> whether there is a better way to accomplish what you are trying to do.
>>>>
>>>> -Matthew
>>>>
>>>> On Thu, Jul 24, 2025 at 5:24 AM Arnav Sabharwal <
>>>> arn...@an...> wrote:
>>>>
>>>>> Hello,
>>>>>
>>>>> I'm trying to tag every instance of a recursive type in a type
>>>>> definition with a tag. This tag is essentially a "type-level natural
>>>>> number". By way of example, here's what I mean:
>>>>>
>>>>> datatype zero = Zero
>>>>> datatype 'n succ = Succ
>>>>>
>>>>> (* example: rose tree *)
>>>>> datatype ('tree, 'list) rose_tree = Node of int * ('list, 'tree) rose_list
>>>>> and ('list, 'tree) rose_list = Nil | Cons of int * ('tree, 'list) rose_list
>>>>>
>>>>> (* example: tree with int list data *)
>>>>> datatype 'list my_list = Nil | Cons of int * 'list my_list
>>>>> and ('tree, 'list) my_tree = Leaf | Node of ('tree, 'list) my_tree * 'list my_list * ('tree, 'list) my_tree
>>>>>
>>>>> As seen, each type is given as many type parameters as is necessary to
>>>>> instantiate its own tag as well as the tags of its "recursive
>>>>> sub-structures". The first type argument is meant for the tag of the
>>>>> recursive type currently being defined.
>>>>>
>>>>> Now, when I use MLton to compile this, the tag types seem to be
>>>>> removed during monomorphization. Thus,
>>>>>
>>>>> (zero, zero succ) rose_tree
>>>>> and
>>>>>
>>>>> (zero succ succ, zero succ succ succ) rose_tree)
>>>>> appear to be the same type in SXML. What are my options here, if I'd
>>>>> like to maintain such a type level distinction? Is XML necessarily the
>>>>> furthest down I can go in the compiler pipeline? I'd greatly appreciate
>>>>> some advice here!
>>>>>
>>>>> Thank you,
>>>>> Arnav.
>>>>> ,
>>>>>
>>>>> To unsubscribe from this group and stop receiving emails from it, send
>>>>> an email to mlt...@ml....
>>>>> _______________________________________________
>>>>> MLton-user mailing list
>>>>> MLt...@li...; mlt...@ml...
>>>>> https://lists.sourceforge.net/lists/listinfo/mlton-user
>>>>>
>>>> To unsubscribe from this group and stop receiving emails from it, send
>> an email to mlt...@ml....
>>
>
>
> --
> -- Yawar Raza
>
>

-- 
-- Yawar Raza

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

Re: [MLton-user] Interplay between empty datatypes and monomorphisation

['Yawar R. (R. Student)' v. MLton-u. <mlt...@ml...>]

Arnav, I think you might need to use "Reply-All" for the reply to remain on
the mailing list, as only Prof. Fluet got your second email (I didn't get
it, at least).

Anyway, I don't think "stopping the MLton compiler part way through" is the
best way to do the sort of thing you're trying to do.

Something you _could_ look into is this one family of SML tricks centered
around http://mlton.org/Fold, possibly more specifically
http://mlton.org/VariableArityPolymorphism. I don't really understand these
libraries though, and I'm personally very averse to this sort of code.

I don't really get what you're trying to do. Why do you have a
generator-generator? Is the generator (output by the generator-generator)
in SML itself or does it just output SML? Does it output just datatype
declarations or complete programs? I think saying what each level inputs
and outputs would be helpful.

In general, you should probably end up doing one of the following:
- Push arity-polymorphism or similarly un-simple stuff up one generator
level, generating different SML source code text for each (rather than
trying to extract MLton compiler output).
- Give up on perfect type safety relating to arities, and just have the
different arities of some things share a single general type.
- Use a different language that either has dependent types (e.g. Idris) or
has more featureful metaprogramming (e.g. F# with its type providers).

But maybe I'm just misunderstanding something. Feel free to ignore those
last two paragraph if so, but I hope those two MLton links above were
useful to learn exist, at least.


On Thursday, July 24, 2025, Matthew Fluet <mat...@gm...> wrote:
>
> Well, if you just want a somewhat normalized representation of the types,
> then you might just use the CoreML representation immediately after
> elaboration (`-keep-pass parseAndElaborate`).
>
> For example:
> ```
> $ cat z.sml
> datatype zero = Zero
> datatype 'n succ = Succ
>
> datatype ('elem, 'index) my_list = Nil | Cons of 'elem * ('elem, 'index)
> my_list
> val z : ((int, zero) my_list, zero succ) my_list = raise Fail "todo"
> $ mlton -keep-pass parseAndElaborate z.sml
> $ tail z.parseAndElaborate.post.core-ml
> (* deadCode: true *)
> (* deadCode: true *)
> (* deadCode: false *)
> datatype zero_21 = Zero_0
> datatype 'a_4547 succ_2 = Succ_0
> datatype ('a_4549, 'a_4548) my_list_0 = Nil_0
>                                         | Cons_0 of 'a_4549
>                                                     * ('a_4549, 'a_4548)
> my_list_0
> val z_26: ((int32, zero_21) my_list_0, zero_21 succ_2) my_list_0 =
>    raise (Fail_0 "todo")
> ```
>
> But, note, you'll still need to see through the uniquification of all
> identifiers.
>
> -Matthew
>
> On Thu, Jul 24, 2025 at 10:48 AM Arnav Sabharwal <arn...@an...>
> wrote:
>
>> Hello Matthew,
>>
>> Thank you for your response! My larger goal here is to make a random
>> generator for (regular) SML inductive types that allows the user to
>> configure "target sizes" for every inductive structure within their type.
>> The type labels are meant to be a way for the user and the tool to agree on
>> a common language for referring to said inductive types.
>>
>> For example, say the user wants to generate 2-d lists where the outer
>> list has length 3 and each inner list has length 2. Then, they'd define
>> their list type like so, building towards their monomorphic "final" type:
>> ```
>> datatype ('elem, 'index) my_list = Nil | Cons of 'elem * ('elem, 'index)
>> my_list
>> type final = ((int, zero) my_list, zero succ) my_list
>> ```
>> This way, the user could later provide the lengths [2, 3] and the tool
>> would unambiguously be able to generate the type with the
>> specified constraints.
>>
>> Oh, and I'm writing the "random generator"-generator tool in OCaml. So, I
>> suppose one way could be to parse out the data-type and type declarations
>> from source, while these tags still hang around. But then I'd have to
>> "evaluate" type applications to bring them into a normal form, due to the
>> lingering type variables...which is why I was considering delaying the
>> point at which I "parse into an OCaml representation" as much as possible.
>>
>> Happy to clarify more if necessary, would greatly appreciate your advice!
>>
>> Arnav.
>>
>> On Thu, Jul 24, 2025 at 8:57 AM Matthew Fluet <mat...@gm...>
>> wrote:
>>
>>> Arnav,
>>>
>>> Yes, in SXML ("Simply-typed" XML), there is no polymorphism whatsoever
>>> (for functions or datatypes) and type parameters that do not contribute to
>>> the representation of a datatype will have been eliminated.
>>>
>>> Actually, the SimplfyTypes (http://mlton.org/XMLSimplifyTypes) XML
>>> optimization will have already eliminated these unused type parameters,
>>> before monomorphisation.  The motivation for SimplifyTypes is to avoid code
>>> duplication by monomorphisation that is unnecessary, due to type parameters
>>> that may be present for high-level API reasons, but do not affect the
>>> dynamics because they do not influence the data representation.
>>>
>>> It may be that if you drop SimplifyTypes (compile with `-drop-pass
>>> xmlSimplifyTypes`), then monomorphisation will force different "versions"
>>> of your tagged datatypes to be separately monmorphised, though with the
>>> current heuristics for naming monomorphised variants, you probably won't
>>> get any evidence of the `zero` or `succ` type parameters remaining in the
>>> SXML program.
>>>
>>> Could you say a bit more about your goals?  That might help to inform
>>> whether there is a better way to accomplish what you are trying to do.
>>>
>>> -Matthew
>>>
>>> On Thu, Jul 24, 2025 at 5:24 AM Arnav Sabharwal <arn...@an...>
>>> wrote:
>>>
>>>> Hello,
>>>>
>>>> I'm trying to tag every instance of a recursive type in a type
>>>> definition with a tag. This tag is essentially a "type-level natural
>>>> number". By way of example, here's what I mean:
>>>>
>>>> datatype zero = Zero
>>>> datatype 'n succ = Succ
>>>>
>>>> (* example: rose tree *)
>>>> datatype ('tree, 'list) rose_tree = Node of int * ('list, 'tree) rose_list
>>>> and ('list, 'tree) rose_list = Nil | Cons of int * ('tree, 'list) rose_list
>>>>
>>>> (* example: tree with int list data *)
>>>> datatype 'list my_list = Nil | Cons of int * 'list my_list
>>>> and ('tree, 'list) my_tree = Leaf | Node of ('tree, 'list) my_tree * 'list my_list * ('tree, 'list) my_tree
>>>>
>>>> As seen, each type is given as many type parameters as is necessary to
>>>> instantiate its own tag as well as the tags of its "recursive
>>>> sub-structures". The first type argument is meant for the tag of the
>>>> recursive type currently being defined.
>>>>
>>>> Now, when I use MLton to compile this, the tag types seem to be removed
>>>> during monomorphization. Thus,
>>>>
>>>> (zero, zero succ) rose_tree
>>>> and
>>>>
>>>> (zero succ succ, zero succ succ succ) rose_tree)
>>>> appear to be the same type in SXML. What are my options here, if I'd
>>>> like to maintain such a type level distinction? Is XML necessarily the
>>>> furthest down I can go in the compiler pipeline? I'd greatly appreciate
>>>> some advice here!
>>>>
>>>> Thank you,
>>>> Arnav.
>>>> ,
>>>>
>>>> To unsubscribe from this group and stop receiving emails from it, send
>>>> an email to mlt...@ml....
>>>> _______________________________________________
>>>> MLton-user mailing list
>>>> MLt...@li...; mlt...@ml...
>>>> https://lists.sourceforge.net/lists/listinfo/mlton-user
>>>>
>>> To unsubscribe from this group and stop receiving emails from it, send
> an email to mlt...@ml....
>


-- 
-- Yawar Raza

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

Re: [MLton-user] Interplay between empty datatypes and monomorphisation

[Matthew F. <mat...@gm...>]

Well, if you just want a somewhat normalized representation of the types,
then you might just use the CoreML representation immediately after
elaboration (`-keep-pass parseAndElaborate`).

For example:
```
$ cat z.sml
datatype zero = Zero
datatype 'n succ = Succ

datatype ('elem, 'index) my_list = Nil | Cons of 'elem * ('elem, 'index)
my_list
val z : ((int, zero) my_list, zero succ) my_list = raise Fail "todo"
$ mlton -keep-pass parseAndElaborate z.sml
$ tail z.parseAndElaborate.post.core-ml
(* deadCode: true *)
(* deadCode: true *)
(* deadCode: false *)
datatype zero_21 = Zero_0
datatype 'a_4547 succ_2 = Succ_0
datatype ('a_4549, 'a_4548) my_list_0 = Nil_0
                                        | Cons_0 of 'a_4549
                                                    * ('a_4549, 'a_4548)
my_list_0
val z_26: ((int32, zero_21) my_list_0, zero_21 succ_2) my_list_0 =
   raise (Fail_0 "todo")
```

But, note, you'll still need to see through the uniquification of all
identifiers.

-Matthew

On Thu, Jul 24, 2025 at 10:48 AM Arnav Sabharwal <arn...@an...>
wrote:

> Hello Matthew,
>
> Thank you for your response! My larger goal here is to make a random
> generator for (regular) SML inductive types that allows the user to
> configure "target sizes" for every inductive structure within their type.
> The type labels are meant to be a way for the user and the tool to agree on
> a common language for referring to said inductive types.
>
> For example, say the user wants to generate 2-d lists where the outer list
> has length 3 and each inner list has length 2. Then, they'd define their
> list type like so, building towards their monomorphic "final" type:
> ```
> datatype ('elem, 'index) my_list = Nil | Cons of 'elem * ('elem, 'index)
> my_list
> type final = ((int, zero) my_list, zero succ) my_list
> ```
> This way, the user could later provide the lengths [2, 3] and the tool
> would unambiguously be able to generate the type with the
> specified constraints.
>
> Oh, and I'm writing the "random generator"-generator tool in OCaml. So, I
> suppose one way could be to parse out the data-type and type declarations
> from source, while these tags still hang around. But then I'd have to
> "evaluate" type applications to bring them into a normal form, due to the
> lingering type variables...which is why I was considering delaying the
> point at which I "parse into an OCaml representation" as much as possible.
>
> Happy to clarify more if necessary, would greatly appreciate your advice!
>
> Arnav.
>
> On Thu, Jul 24, 2025 at 8:57 AM Matthew Fluet <mat...@gm...>
> wrote:
>
>> Arnav,
>>
>> Yes, in SXML ("Simply-typed" XML), there is no polymorphism whatsoever
>> (for functions or datatypes) and type parameters that do not contribute to
>> the representation of a datatype will have been eliminated.
>>
>> Actually, the SimplfyTypes (http://mlton.org/XMLSimplifyTypes) XML
>> optimization will have already eliminated these unused type parameters,
>> before monomorphisation.  The motivation for SimplifyTypes is to avoid code
>> duplication by monomorphisation that is unnecessary, due to type parameters
>> that may be present for high-level API reasons, but do not affect the
>> dynamics because they do not influence the data representation.
>>
>> It may be that if you drop SimplifyTypes (compile with `-drop-pass
>> xmlSimplifyTypes`), then monomorphisation will force different "versions"
>> of your tagged datatypes to be separately monmorphised, though with the
>> current heuristics for naming monomorphised variants, you probably won't
>> get any evidence of the `zero` or `succ` type parameters remaining in the
>> SXML program.
>>
>> Could you say a bit more about your goals?  That might help to inform
>> whether there is a better way to accomplish what you are trying to do.
>>
>> -Matthew
>>
>> On Thu, Jul 24, 2025 at 5:24 AM Arnav Sabharwal <arn...@an...>
>> wrote:
>>
>>> Hello,
>>>
>>> I'm trying to tag every instance of a recursive type in a type
>>> definition with a tag. This tag is essentially a "type-level natural
>>> number". By way of example, here's what I mean:
>>>
>>> datatype zero = Zero
>>> datatype 'n succ = Succ
>>>
>>> (* example: rose tree *)
>>> datatype ('tree, 'list) rose_tree = Node of int * ('list, 'tree) rose_list
>>> and ('list, 'tree) rose_list = Nil | Cons of int * ('tree, 'list) rose_list
>>>
>>> (* example: tree with int list data *)
>>> datatype 'list my_list = Nil | Cons of int * 'list my_list
>>> and ('tree, 'list) my_tree = Leaf | Node of ('tree, 'list) my_tree * 'list my_list * ('tree, 'list) my_tree
>>>
>>> As seen, each type is given as many type parameters as is necessary to
>>> instantiate its own tag as well as the tags of its "recursive
>>> sub-structures". The first type argument is meant for the tag of the
>>> recursive type currently being defined.
>>>
>>> Now, when I use MLton to compile this, the tag types seem to be removed
>>> during monomorphization. Thus,
>>>
>>> (zero, zero succ) rose_tree
>>> and
>>>
>>> (zero succ succ, zero succ succ succ) rose_tree)
>>> appear to be the same type in SXML. What are my options here, if I'd
>>> like to maintain such a type level distinction? Is XML necessarily the
>>> furthest down I can go in the compiler pipeline? I'd greatly appreciate
>>> some advice here!
>>>
>>> Thank you,
>>> Arnav.
>>> ,
>>>
>>> To unsubscribe from this group and stop receiving emails from it, send
>>> an email to mlt...@ml....
>>> _______________________________________________
>>> MLton-user mailing list
>>> MLt...@li...; mlt...@ml...
>>> https://lists.sourceforge.net/lists/listinfo/mlton-user
>>>
>>

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

Re: [MLton-user] Interplay between empty datatypes and monomorphisation

[Arnav S. <arn...@an...>]

Hello Matthew,

Thank you for your response! My larger goal here is to make a random
generator for (regular) SML inductive types that allows the user to
configure "target sizes" for every inductive structure within their type.
The type labels are meant to be a way for the user and the tool to agree on
a common language for referring to said inductive types.

For example, say the user wants to generate 2-d lists where the outer list
has length 3 and each inner list has length 2. Then, they'd define their
list type like so, building towards their monomorphic "final" type:
```
datatype ('elem, 'index) my_list = Nil | Cons of 'elem * ('elem, 'index)
my_list
type final = ((int, zero) my_list, zero succ) my_list
```
This way, the user could later provide the lengths [2, 3] and the tool
would unambiguously be able to generate the type with the
specified constraints.

Oh, and I'm writing the "random generator"-generator tool in OCaml. So, I
suppose one way could be to parse out the data-type and type declarations
from source, while these tags still hang around. But then I'd have to
"evaluate" type applications to bring them into a normal form, due to the
lingering type variables...which is why I was considering delaying the
point at which I "parse into an OCaml representation" as much as possible.

Happy to clarify more if necessary, would greatly appreciate your advice!

Arnav.

On Thu, Jul 24, 2025 at 8:57 AM Matthew Fluet <mat...@gm...>
wrote:

> Arnav,
>
> Yes, in SXML ("Simply-typed" XML), there is no polymorphism whatsoever
> (for functions or datatypes) and type parameters that do not contribute to
> the representation of a datatype will have been eliminated.
>
> Actually, the SimplfyTypes (http://mlton.org/XMLSimplifyTypes) XML
> optimization will have already eliminated these unused type parameters,
> before monomorphisation.  The motivation for SimplifyTypes is to avoid code
> duplication by monomorphisation that is unnecessary, due to type parameters
> that may be present for high-level API reasons, but do not affect the
> dynamics because they do not influence the data representation.
>
> It may be that if you drop SimplifyTypes (compile with `-drop-pass
> xmlSimplifyTypes`), then monomorphisation will force different "versions"
> of your tagged datatypes to be separately monmorphised, though with the
> current heuristics for naming monomorphised variants, you probably won't
> get any evidence of the `zero` or `succ` type parameters remaining in the
> SXML program.
>
> Could you say a bit more about your goals?  That might help to inform
> whether there is a better way to accomplish what you are trying to do.
>
> -Matthew
>
> On Thu, Jul 24, 2025 at 5:24 AM Arnav Sabharwal <arn...@an...>
> wrote:
>
>> Hello,
>>
>> I'm trying to tag every instance of a recursive type in a type definition
>> with a tag. This tag is essentially a "type-level natural number". By way
>> of example, here's what I mean:
>>
>> datatype zero = Zero
>> datatype 'n succ = Succ
>>
>> (* example: rose tree *)
>> datatype ('tree, 'list) rose_tree = Node of int * ('list, 'tree) rose_list
>> and ('list, 'tree) rose_list = Nil | Cons of int * ('tree, 'list) rose_list
>>
>> (* example: tree with int list data *)
>> datatype 'list my_list = Nil | Cons of int * 'list my_list
>> and ('tree, 'list) my_tree = Leaf | Node of ('tree, 'list) my_tree * 'list my_list * ('tree, 'list) my_tree
>>
>> As seen, each type is given as many type parameters as is necessary to
>> instantiate its own tag as well as the tags of its "recursive
>> sub-structures". The first type argument is meant for the tag of the
>> recursive type currently being defined.
>>
>> Now, when I use MLton to compile this, the tag types seem to be removed
>> during monomorphization. Thus,
>>
>> (zero, zero succ) rose_tree
>> and
>>
>> (zero succ succ, zero succ succ succ) rose_tree)
>> appear to be the same type in SXML. What are my options here, if I'd like
>> to maintain such a type level distinction? Is XML necessarily the furthest
>> down I can go in the compiler pipeline? I'd greatly appreciate some advice
>> here!
>>
>> Thank you,
>> Arnav.
>> ,
>>
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to mlt...@ml....
>> _______________________________________________
>> MLton-user mailing list
>> MLt...@li...; mlt...@ml...
>> https://lists.sourceforge.net/lists/listinfo/mlton-user
>>
>

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....

Re: [MLton-user] Interplay between empty datatypes and monomorphisation

[Matthew F. <mat...@gm...>]

Arnav,

Yes, in SXML ("Simply-typed" XML), there is no polymorphism whatsoever (for
functions or datatypes) and type parameters that do not contribute to the
representation of a datatype will have been eliminated.

Actually, the SimplfyTypes (http://mlton.org/XMLSimplifyTypes) XML
optimization will have already eliminated these unused type parameters,
before monomorphisation.  The motivation for SimplifyTypes is to avoid code
duplication by monomorphisation that is unnecessary, due to type parameters
that may be present for high-level API reasons, but do not affect the
dynamics because they do not influence the data representation.

It may be that if you drop SimplifyTypes (compile with `-drop-pass
xmlSimplifyTypes`), then monomorphisation will force different "versions"
of your tagged datatypes to be separately monmorphised, though with the
current heuristics for naming monomorphised variants, you probably won't
get any evidence of the `zero` or `succ` type parameters remaining in the
SXML program.

Could you say a bit more about your goals?  That might help to inform
whether there is a better way to accomplish what you are trying to do.

-Matthew

On Thu, Jul 24, 2025 at 5:24 AM Arnav Sabharwal <arn...@an...>
wrote:

> Hello,
>
> I'm trying to tag every instance of a recursive type in a type definition
> with a tag. This tag is essentially a "type-level natural number". By way
> of example, here's what I mean:
>
> datatype zero = Zero
> datatype 'n succ = Succ
>
> (* example: rose tree *)
> datatype ('tree, 'list) rose_tree = Node of int * ('list, 'tree) rose_list
> and ('list, 'tree) rose_list = Nil | Cons of int * ('tree, 'list) rose_list
>
> (* example: tree with int list data *)
> datatype 'list my_list = Nil | Cons of int * 'list my_list
> and ('tree, 'list) my_tree = Leaf | Node of ('tree, 'list) my_tree * 'list my_list * ('tree, 'list) my_tree
>
> As seen, each type is given as many type parameters as is necessary to
> instantiate its own tag as well as the tags of its "recursive
> sub-structures". The first type argument is meant for the tag of the
> recursive type currently being defined.
>
> Now, when I use MLton to compile this, the tag types seem to be removed
> during monomorphization. Thus,
>
> (zero, zero succ) rose_tree
> and
>
> (zero succ succ, zero succ succ succ) rose_tree)
> appear to be the same type in SXML. What are my options here, if I'd like
> to maintain such a type level distinction? Is XML necessarily the furthest
> down I can go in the compiler pipeline? I'd greatly appreciate some advice
> here!
>
> Thank you,
> Arnav.
> ,
>
> To unsubscribe from this group and stop receiving emails from it, send an
> email to mlt...@ml....
> _______________________________________________
> MLton-user mailing list
> MLt...@li...; mlt...@ml...
> https://lists.sourceforge.net/lists/listinfo/mlton-user
>

To unsubscribe from this group and stop receiving emails from it, send an email to mlt...@ml....