5 ms·

I really like the idea of canonical maps/morphisms. The idea is that there exists one and only one possible implementation of a given type transformation. For c

I really like the idea of canonical maps/morphisms. The idea is that there exists one and only one possible implementation of a given type transformation. For code constructed of canonical morphisms, the compiler can prove correctness. As an example, there are infinitely many maps from u32 -> u32. But only one map from Minutes -> Seconds. If you use u32 for your times, you need to rely on tests for confidence you have the right math. But if you use Minutes and Seconds, you can rely on the compiler to prove correctness.

dullcrisp 3y ago
Couldn’t you lift any of your u32 -> u32 maps to a map from Minutes -> Minutes or Seconds -> Seconds and then compose with your canonical map to get a different Minutes -> Seconds map? Edit: you did say canonical and not unique so I’m probably just being pedantic.
tialaramex 3y ago
> As an example, there are infinitely many maps from u32 -> u32. But only one map from Minutes -> Seconds I see where you're coming from, but I think this is only superficially appealing, there's no meat to it. The obvious u32 -> u32 map is identity, in the same way Minutes -> Seconds is a multiplication by sixty, but it's actually not hard to imagine other mappings for the Minutes -> Seconds either, how about given how many Minutes I've been roasting the turkey, how many Seconds should it be rested before carving? In reality what Rust did here was to offer a Duration type and an Instant type, representing the idea of a period of time (a duration) or a specific moment in time (an instant) and then leverage this idea to have functions like std::thread::sleep take a Duration, so the question of whether we sleep in minutes, second, nanoyears or whatever isn't a question for the sleep function. Edited to add: These are also important because they're Vocabulary types. By being provided in the standard library (Duration is actually even in core, so it's available on your embedded Rust) these types encourage everybody to agree on vocabulary and enrich the entire ecosystem. Instead of Jim Bob's library working in microseconds and Sarah's library using milliseconds, meaning I must convert everywhere and if I get it wrong it causes chaos, they just both use Durations and everything just works.
drewcoo 3y ago
> But only one map from Minutes -> Seconds. Actually, time is difficult. Really difficult. Some minutes on the real world clock do not have 60 seconds.

dullcrisp 3y ago

Couldn’t you lift any of your u32 -> u32 maps to a map from Minutes -> Minutes or Seconds -> Seconds and then compose with your canonical map to get a different Minutes -> Seconds map? Edit: you did say canonical and not unique so I’m probably just being pedantic.

tialaramex 3y ago

> As an example, there are infinitely many maps from u32 -> u32. But only one map from Minutes -> Seconds I see where you're coming from, but I think this is only superficially appealing, there's no meat to it. The obvious u32 -> u32 map is identity, in the same way Minutes -> Seconds is a multiplication by sixty, but it's actually not hard to imagine other mappings for the Minutes -> Seconds either, how about given how many Minutes I've been roasting the turkey, how many Seconds should it be rested before carving? In reality what Rust did here was to offer a Duration type and an Instant type, representing the idea of a period of time (a duration) or a specific moment in time (an instant) and then leverage this idea to have functions like std::thread::sleep take a Duration, so the question of whether we sleep in minutes, second, nanoyears or whatever isn't a question for the sleep function. Edited to add: These are also important because they're Vocabulary types. By being provided in the standard library (Duration is actually even in core, so it's available on your embedded Rust) these types encourage everybody to agree on vocabulary and enrich the entire ecosystem. Instead of Jim Bob's library working in microseconds and Sarah's library using milliseconds, meaning I must convert everywhere and if I get it wrong it causes chaos, they just both use Durations and everything just works.

drewcoo 3y ago

> But only one map from Minutes -> Seconds. Actually, time is difficult. Really difficult. Some minutes on the real world clock do not have 60 seconds.