依赖于数据类型的类型

Question

我在编写一个只能在一周中的特定几天传递的函数时遇到了一些困难。我预计这会起作用：

datatype days = sunday | monday | tuesday | wednesday | thursday | friday | saturday

fn only_sunday{d:days | d == sunday}(d: days(d)): days(d) = d

当然，days(d) 从未被定义过。这似乎只是可行，因为 ATS 有很多内置类型 - int 和 int(int)，等等

这也行不通，也许只是语法错误？

typedef only_sunday = { d:days | d == sunday }

fn only_sunday(d: only_sunday): only_sunday = d

重温 Introduction to Programming in ATS 的依赖类型一章后，我意识到这是可行的：

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))

但是，当然，n == 0 意味着 "the day must be sunday" 比 d == sunday 这样的代码更不清楚。尽管将天数映射到数字似乎并不罕见，但请考虑：

datatype toppings(int) = lettuce(0) | swiss_cheese(1) | mushrooms(2) | ...

在这种情况下，数字是完全没有意义的，因此如果您手头有数据类型定义，您只能将任何 {n:int | n != 1} ... toppings(n) 代码理解为反瑞士奶酪。如果你要编辑一个新的浇头

datatype toppings(int) = lettuce(0) | tomatoes(1) | swiss_cheese(2) | ...

那么仅在任何瑞士奶酪代码中将 1 更新为 2 将是一项繁琐的工作。

是否有更符号化的方式来使用依赖类型？

Answer 1

您可以尝试这样的操作：

stadef lettuce = 0
stadef swiss_cheese = 1
stadef mushrooms = 2

datatype
toppings(int) =
| lettuce(lettuce)
| swiss_cheese(swiss_cheese)
| mushrooms(mushrooms)

依赖于数据类型的类型

Dependent types over datatypes

dependent-type

ats