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....