[Ur] Metaprogramming doubt

[Saulo Araujo]

Hi,

I am studying how to do metaprogramming in Ur/Web. After reading the
"Type-Level Computation" tutorial (
http://www.impredicative.com/ur/tutorial/tlc.html), part of the "Ur:
Statically-Typed Metaprogramming with Type-Level Record Computation" paper (
http://adam.chlipala.net/papers/UrPLDI10/UrPLDI10.pdf) and also looking
into the "Ur/Web People Organizer" source code (
https://github.com/achlipala/upo) I was able to define a functor that
receives three tables as arguments:

con unitify recordType = map (fn _ => ()) recordType

functor Make (M : sig
          con groupTablePrimaryKeyColumns :: {Type}
          con groupTableOtherColumns :: {Type}
          constraint groupTablePrimaryKeyColumns ~
groupTableOtherColumns
          con groupTableOtherConstraints :: {{Unit}}
          constraint [Pkey = unitify groupTablePrimaryKeyColumns] ~
groupTableOtherConstraints
          val groupTable : sql_table (groupTablePrimaryKeyColumns ++
groupTableOtherColumns)
                         ([Pkey = unitify groupTablePrimaryKeyColumns] ++
groupTableOtherConstraints)

          con rowTablePrimaryKeyColumns :: {Type}
          con rowTableOtherColumns :: {Type}
          constraint rowTablePrimaryKeyColumns ~ rowTableOtherColumns

          con rowTableOtherConstraints :: {{Unit}}
          constraint [Pkey = unitify rowTablePrimaryKeyColumns] ~
rowTableOtherConstraints
          val rowTable : sql_table (rowTablePrimaryKeyColumns ++
rowTableOtherColumns)
                       ([Pkey = unitify rowTablePrimaryKeyColumns] ++
rowTableOtherConstraints)

          con groupRowTablePrimaryKeyColumns :: {Type}
          con groupRowTableOtherColumns :: {Type}
          constraint groupRowTablePrimaryKeyColumns ~
groupRowTableOtherColumns

          con groupRowTableOtherConstraints :: {{Unit}}
          constraint [Pkey = unitify groupRowTablePrimaryKeyColumns] ~
groupRowTableOtherConstraints

          val groupRowTable : sql_table (groupRowTablePrimaryKeyColumns ++
groupRowTableOtherColumns)
                         ([Pkey = unitify groupRowTablePrimaryKeyColumns]
++ groupRowTableOtherConstraints)
          end) = struct
end

table projectTable : {Id : int, Nm : string} PRIMARY KEY Id

table taskTable : {Id : int, Nm : string} PRIMARY KEY Id

table projectTaskTable : {ProjectId : int, TaskId : int} PRIMARY KEY
(ProjectId, TaskId),
      CONSTRAINT PROJECT_ID_IS_FOREIGN_KEY FOREIGN KEY ProjectId REFERENCES
projectTable (Id),
      CONSTRAINT TASK_ID_IS_FOREIGN_KEY FOREIGN KEY TaskId REFERENCES
taskTable (Id)

structure M = Make (struct
            val groupTable = projectTaskTable
            val rowTable = taskTable
            val groupRowTable = projectTaskTable
            end)

However, this functor is too permissive, because one can pass to it any
three tables. Does the Ur/Web type system allow me to require that
groupRowTable contains foreign keys to the group and row tables? If so,
could you show me how or point me to a similar example?

Sincerely,
Saulo Araujo
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.impredicative.com/pipermail/ur/attachments/20160926/9901ead2/attachment.html>