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