Re: [Ur] Better date & time support in Ur/Web + PostgreSQL

[Adam Chlipala]

Thanks for sharing the description of your new functionality, at my 
request in a GitHub issue ! 
It looks like there are no related strong opinions lurking on this 
mailing list.


I would definitely be up to seeing appropriate types built into the 
standard library (and compiler). Are there natural implementations for 
the other major open-source SQL engines, not just Postgres?


On 8/16/20 9:56 AM, Simon Van Casteren wrote:


I've been building www.classy.school  for 
some time with Ur/Web now. It's an application for music schools and a 
lot of it revolves around schedules: Who has lessons at what time, 
which teacher, which room, etc etc.


In Ur/Web's "standard library" there are 2 types to represent dates / 
times:


  * Basis.time (Corresponds to unix epoch milliseconds IIRC). Contains
both date and time
  * Datetime.t (Corresponds to a C struct IIRC). A bit more structure
than Basis.time

I don't work with these two types at all. I defined two other types:

  * calendardate. This is actually a type synonym for Basis.time, but
only because it makes it possible to serialize this to sql values.
All operations on this type only change the date part, so year -
month - day. It contains no timezone info.
  * clocktime: { Hour: int, Minute: int}. (I don't need seconds, but
it wouldn't hurt to add it as well). I have to serialize /
deserialize this whenever it goes into the DB, very annoying.

I've found this to be a much easier representation to work with for my 
domain. Example: When you enroll with a teacher for some private 
lessons, you often do it for x (eg: 10) lessons on a certain weekday 
on a certain time. This time I have in my datamodel as a clocktime. 
The actual "timestamps" of every lesson are seperate. Another benefit: 
Comparing calendardates is much easier than comparing Basis.time / 
Datetime.t.


Anyway, I've been thinking for some time to propose to upstream all of 
this / some of this into the standard library, if there is any 
interest for it. With that I'd also serialize them into the correct 
PostgreSQL types (calendardate -> date, clocktime -> time without 
timezone). Afterwards, I want to look into adding support for some SQL 
operators on these, especially adding a clocktime to a date (which 
then becomes a PostgreSQL timestamp without timezone, not sure yet how 
to model this in the type system). Being able to do this in SQL would 
be huge for my application.


So long story short, I'd mainly like to know if adding this stuff to 
the standard library would be welcomed. If not, I'll keep all this in 
my personal repo and put the SQL stuff in my urweb fork, but I thought 
I'd ask :).


Simon



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

[Ur] Better date & time support in Ur/Web + PostgreSQL

[Simon Van Casteren]

I've been building www.classy.school for some time with Ur/Web now. It's an
application for music schools and a lot of it revolves around schedules:
Who has lessons at what time, which teacher, which room, etc etc.

In Ur/Web's "standard library" there are 2 types to represent dates / times:

   - Basis.time (Corresponds to unix epoch milliseconds IIRC). Contains
   both date and time
   - Datetime.t (Corresponds to a C struct IIRC). A bit more structure than
   Basis.time

I don't work with these two types at all. I defined two other types:

   - calendardate. This is actually a type synonym for Basis.time, but only
   because it makes it possible to serialize this to sql values. All
   operations on this type only change the date part, so year - month - day.
   It contains no timezone info.
   - clocktime: { Hour: int, Minute: int}. (I don't need seconds, but it
   wouldn't hurt to add it as well). I have to serialize / deserialize this
   whenever it goes into the DB, very annoying.

I've found this to be a much easier representation to work with for my
domain. Example: When you enroll with a teacher for some private lessons,
you often do it for x (eg: 10) lessons on a certain weekday on a certain
time. This time I have in my datamodel as a clocktime. The actual
"timestamps" of every lesson are seperate. Another benefit: Comparing
calendardates is much easier than comparing Basis.time / Datetime.t.

Anyway, I've been thinking for some time to propose to upstream all of this
/ some of this into the standard library, if there is any interest for it.
With that I'd also serialize them into the correct PostgreSQL types
(calendardate -> date, clocktime -> time without timezone). Afterwards, I
want to look into adding support for some SQL operators on these,
especially adding a clocktime to a date (which then becomes a PostgreSQL
timestamp without timezone, not sure yet how to model this in the type
system). Being able to do this in SQL would be huge for my application.

So long story short, I'd mainly like to know if adding this stuff to the
standard library would be welcomed. If not, I'll keep all this in my
personal repo and put the SQL stuff in my urweb fork, but I thought I'd ask
:).

Simon
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur