I struggled for a bit with writing a function that could only be passed certain days of the week. I expected that this would work:
datatype days = sunday | monday | tuesday | wednesday | thursday | friday | saturday
fn only_sunday{d:days | d == sunday}(d: days(d)): days(d) = d
but of course, days(d) was never even defined. That only seemed like it would work because ATS has so many builtin types - int and also int(int), etc.
This also doesn't work, but perhaps it's just the syntax that's wrong?
typedef only_sunday = { d:days | d == sunday }
fn only_sunday(d: only_sunday): only_sunday = d
After revisiting the Dependent Types chapter of Introduction to Programming in ATS, I realized that this works:
datatype days(int) =
| sunday(0)
| monday(1)
| tuesday(2)
| wednesday(3)
| thursday(4)
| friday(5)
| saturday(6)
fn print_days{n:int}(d: days(n)): void =
print_string(case+ d of
| sunday() => "sunday"
| monday() => "monday"
| tuesday() => "tuesday"
| wednesday() => "wednesday"
| thursday() => "thursday"
| friday() => "friday"
| saturday() => "saturday")
overload print with print_days
fn sunday_only{n:int | n == 0}(d: days(n)): days(n) = d
implement main0() =
println!("this typechecks: ", sunday_only(sunday))
but of course, it's a little bit less clear that n == 0 means "the day must be sunday" than it would with some code like d == sunday. And although it doesn't seem that unusual to map days to numbers, consider:
datatype toppings(int) = lettuce(0) | swiss_cheese(1) | mushrooms(2) | ...
In this case the numbers are completely senseless, such that you can only understand any {n:int | n != 1} ... toppings(n) code as anti-swiss-cheese if you have the datatype definition at hand. And if you were to edit in a new topping
datatype toppings(int) = lettuce(0) | tomatoes(1) | swiss_cheese(2) | ...
then it would be quite a chore update 1 to 2 in only any Swiss cheese code.
Is there a more symbolic way to use dependent types?
You could try something like this:
stadef lettuce = 0
stadef swiss_cheese = 1
stadef mushrooms = 2
datatype
toppings(int) =
| lettuce(lettuce)
| swiss_cheese(swiss_cheese)
| mushrooms(mushrooms)