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