[Ur] common type for different functor instantiations
Adam Chlipala
adamc at impredicative.com
Thu Oct 27 08:21:48 EDT 2011
Gergely Buday wrote:
>> Sure: define [mRecord] outside the functor completely. It could be an
>> abstract type in an enclosing module. (Modules can contain functors, which
>> can contain modules that contain functors, and so on ad infinitum.)
>>
> Thinking about how to define the abstract type concretely, I would have
>
> structure Enclosing =
> struct
>
> datatype mRecord = First of $firstFields |
> Second of $secondFields |
> Third of $thirdFields
>
> datatype whichmodule = FirstM | SecondM | ThirdM
>
> functor Render ( M: sig ... val module : whichmodule ... end ) : Signature =
> struct
> ...
> end
>
> end
>
> Do you agree with this, or, you would suggest something else?
>
There's nothing obviously wrong with that code, except that you might
want to add an explicit signature ascription to [Enclosing], depending
on whether some .urs file is already ascribing a signature.
It _is_ suspicious that you seem to be writing a functor designed only
to be used on one of three arguments. I'd consider using polymorphism
to permit the functor to work in more cases, even if you only plan to
apply it to three known arguments.
More information about the Ur
mailing list