[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