Fun little project

[wizard7377]

For reasons known not by me, I have started trying to port Twelf... to OCaml... using Github Copilot
If you were by some chance interested in that very idea, it is here: https://github.com/wizard7377/twelf/tree/main

Best,
Asher Frost

[robsimmons]

best of luck!

[wizard7377]

Update, got all the syntax working: https://github.com/wizard7377/twelf

[wizard7377]

For anyone that happens to know: there are a lot of comments of the form (*! ... !*) (particuarly around modules). What is the purpose of them?

[robsimmons]

Looking at the git history, these seem like they were mostly due to a refactor that Carsten did between Twelf 1.3 and Twelf 1.4 — I'd treat them as regular commented-out-dead-code.

[frankpfenning]

Below is my recollection. When this project started, Carsten and I experimented with a fully functorized style of SML programming. However, this lead to some problems with sharing constraints, as specified in the "Definition of Standard ML". Plus, there where many redundancies in places where a module was only instantiated once. So eventually we backtracked somewhat, using some structures more pervasively. Instead of deleting references to (more or less) pervasive structures, we commented the functor parameters in the (*! ... !*) style so it is recorded which structures a structure or functor actually depends on (even if it is not an explicit parameter). We didn't do this consistently throughout, and, as a comment, it cannot be enforced by the SML compiler. Nowadays in my programming, I use explicit parameters more selectively, when there are (or I anticipate) multiple instances. - Frank

…

On Mon, Dec 29, 2025 at 9:28 AM Asher Frost ***@***.***> wrote: For anyone that happens to know: there are a lot of comments of the form (*! ... !*) (particuarly around modules). What is the purpose of them? — Reply to this email directly, view it on GitHub <#82 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAHKJ7LBEEM2BRSS6G6H42T4EE263AVCNFSM6AAAAACNTTDCVSVHI2DSMVQWIX3LMV43URDJONRXK43TNFXW4Q3PNVWWK3TUHMYTKMZWGYZTGMQ> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

-- Frank Pfenning, Professor Computer Science Department Carnegie Mellon University Pittsburgh, PA 15213-3891 http://www.cs.cmu.edu/~fp https://cmu.zoom.us/my/fpfenning +1 412 268-6343 GHC 6017

[wizard7377]

On a related style note, is their a convention for capitalization of pattern variables?

[wizard7377]

Also (as a side note) I've decided that it will be advantageous to work on a way to actually convert SML programattically to OCaml, found here

[frankpfenning]

How far along is this project? I may have some use of it for another purpose. What I need does not include the module system, mutable store, or exceptions, so it is relatively basic. Thanks, Frank

…

On Thu, Jan 1, 2026 at 10:53 AM Asher Frost ***@***.***> wrote: Also (as a side note) I've decided that it will be advantageous to work on a way to actually convert SML programattically to OCaml, found here <https://github.com/wizard7377/sml-ocaml-converter> — Reply to this email directly, view it on GitHub <#82 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAHKJ7OSDBR5KXDZYSZS2K34EU7ITAVCNFSM6AAAAACNTTDCVSVHI2DSMVQWIX3LMV43URDJONRXK43TNFXW4Q3PNVWWK3TUHMYTKMZYGY2DMNA> . You are receiving this because you commented.Message ID: ***@***.***>

-- Frank Pfenning, Professor Computer Science Department Carnegie Mellon University Pittsburgh, PA 15213-3891 http://www.cs.cmu.edu/~fp https://cmu.zoom.us/my/fpfenning +1 412 268-6343 GHC 6017

[wizard7377]

@frankpfenning do your files follow OCaml naming conventions? If they do, I can get a converter running much quicker

[wizard7377]

@frankpfenning in the case you're still working on this, I've started work on a companion project, https://github.com/wizard7377/basis, which is an attempt to port the SML basis library to OCaml (this one is in its very early stages, the SML -> OCaml converter proper should be just about ready for use, especially if you stick to non-extended and idiomatic SML)

[robsimmons]

There's very little chance Twelf follows the OCaml naming conventions, as it probably predates those conventions by quite a bit 😄

[wizard7377]

There's very little chance Twelf follows the OCaml naming conventions, as it probably predates those conventions by quite a bit 😄

Yep it does not... fortunately I've managed to get most (I'm not sure that without completly re-implementing the entire SML frontend it would be possible to do better) names down.
This comes from a couple key observations.

1. There are ways to make sure that every name is unique (I chose the method where if a name is NAME_, then it becomes NAME__, and if the name is changed (ie, possibly already in scope) an underscore is added)
2. All of type variables, type constructors, constructor and value declarations (not usages), modules, module types, module variables are all unambiguous
3. Thus, the only things that are ambiguous are variables, values, and constructors in patterns in expressions
4. Pattern heads aren't actually ambiguous, as they must be constructors (technically also pattern aliases but that's a different story)
5. Qualified names are never variables, which means that in a pattern they are constructors and in an expression the names... are ambiguous
6. Most pattern variables actually follow a pretty standard naming convention: [a-zA-Z]s?[0-9]?'?
7. Using all the afore, we can completely accurately transform the module language, all types, as well as most patterns

Of course, this can't deal with expressions... as far as I can tell, there is not an easy way to determine if an expression has the correct capitalization. This is because while in a pattern the names all need to be simple constructors or variables, which are difficult but with enough duct tape usually possible to detect. The same solution cannot be said for values however. Consider a module like formatter.formatter, getting every use of the names right would require through threading through state throughout the files.

Fourtanetly, this actually isn't that big of a problem... sort of. Basically, at this point I realized that most of SML will probably not convert perfectly, there are just too many differences between the languages. However, even getting most of the conversions to be syntactically valid would be a huge head start. Currently, I'm at, out of the 270 file codebase (for the library only)

• 187 syntactically well formed programs in OCaml
• 77 ill formed programs but still converted
• 6 programs that fail to convert at all
  Definitely needs more work, but with a codebase that's more style compliant the results are probably much better

Also, is it valid to use an infix operator as a regular function in SML (without preceding it with op)? The standard implies that it is valid,

[wizard7377]

Update on the update, 220 well formed ocaml files and counting!

[wizard7377]

Progress might be slowing down in the next couple days, what with college apps and exams, so I expect this will be done sometime next week, possibly a little earlier

[wizard7377]

First working release is here:
https://github.com/wizard7377/sml-ocaml-converter/tree/v0.0.1
Note that this doesn't deal with comments, or capitalization

[wizard7377]

Code should be just about ready: https://github.com/wizard7377/sml-ocaml-converter/tree/master

[wizard7377]

Project is in large part working and a PR to opam is on the way :) ocaml/opam-repository#29256

[wizard7377]

Is there a way to print all names in scope for SML ?

[wizard7377]

As an aside, here's another fun project of mine that attempts to combine universe levels with phases (a la Racket Scheme) https://github.com/wizard7377/MLTT

[wizard7377]

First correct run, on a (heavily modified) version of the Hamlet source code, is here https://github.com/wizard7377/basis .

[wizard7377]

Just realized I didn't mention this, I'm working on the (hopefully) final iteration of the port of the twelf project (porting twelf itself and correcting the output) hopefully, given the speed at which it's been going, I'll have the codebase building within the week :)

[wizard7377]

@robsimmons @frankpfenning IT BUILDS

untitled.mp4