Hệ thống kiểu trong Scala là Turing hoàn chỉnh. Bằng chứng? Thí dụ? Lợi ích?

Question

Có những tuyên bố rằng hệ thống kiểu của Scala là Turing hoàn tất. Câu hỏi của tôi là:

1. Có bằng chứng chính thức cho điều này không?

2. Làm thế nào một phép tính đơn giản trông giống như trong hệ thống kiểu Scala?

3. Đây có phải là bất kỳ lợi ích nào đối với Scala - ngôn ngữ không? Điều này có khiến Scala trở nên “mạnh mẽ hơn” theo cách nào đó so với các ngôn ngữ không có hệ thống kiểu Turing hoàn chỉnh không?

Tôi đoán điều này áp dụng cho các ngôn ngữ và hệ thống kiểu nói chung.

Answer 1

Có một bài đăng trên blog ở đâu đó với việc thực hiện loại cấp phép tích hợp bộ đệm SKI, được biết là Turing-complete.

Hệ thống kiểu Turing hoàn chỉnh về cơ bản có cùng lợi ích và nhược điểm mà ngôn ngữ Turing hoàn chỉnh có: bạn có thể làm bất cứ điều gì, nhưng bạn có thể chứng minh rất ít. Đặc biệt, bạn không thể chứng minh rằng bạn cuối cùng sẽ thực sự làm điều gì đó.

Một ví dụ về tính toán mức loại là bộ biến đổi bộ sưu tập kiểu bảo quản mới trong Scala 2.8. Trong Scala 2.8, các phương thức như map, filter và như vậy được đảm bảo trả về bộ sưu tập cùng loại mà chúng được gọi. Vì vậy, nếu bạn filter a Set[Int], bạn sẽ quay lại Set[Int] và nếu bạn map a List[String] bạn nhận lại List[Whatever the return type of the anonymous function is].

Bây giờ, như bạn thấy, map thực sự có thể chuyển đổi loại phần tử. Vì vậy, điều gì sẽ xảy ra nếu loại phần tử mới không thể được biểu diễn bằng loại bộ sưu tập gốc? Ví dụ: BitSet chỉ có thể chứa số nguyên cố định chiều rộng. Vì vậy, điều gì sẽ xảy ra nếu bạn có một số BitSet[Short] và bạn ánh xạ từng số tới biểu diễn chuỗi của nó?

someBitSet map { _.toString() } 

Kết quả sẽ là một BitSet[String], nhưng điều đó là không thể. Vì vậy, Scala chọn siêu kiểu có nguồn gốc xuất sắc nhất của BitSet, có thể giữ String, trong trường hợp này là Set[String].

Tất cả các tính toán này đang xảy ra trong suốt thời gian biên dịch , hay chính xác hơn trong loại kiểm tra thời gian, sử dụng chức năng loại cấp. Vì vậy, nó được đảm bảo tĩnh để được loại an toàn, mặc dù các loại được thực sự tính toán và do đó không được biết đến tại thời điểm thiết kế.

Answer 2

My blog post khi mã hóa phép tính SKI trong hệ thống kiểu Scala hiển thị đầy đủ tính năng Turing.

Đối với một số tính toán cấp kiểu đơn giản, cũng có một số ví dụ về cách mã hóa các số tự nhiên và bổ sung/multiplication.

Cuối cùng, có một tuyệt vời series of articles về lập trình cấp loại trên blog của Apocalisp.