2011-12-13 15 views
24

Scala sử dụng hệ thống kiểu dựa trên Hệ thống F ω, thường được cho là chuẩn hóa mạnh mẽ. Tối ưu hóa mạnh mẽ ngụ ý hoàn toàn không Turing.Thuộc tính nào của hệ thống kiểu Scala làm cho nó hoàn thành Turing?

Tuy nhiên, hệ thống kiểu của Scala là Turing-complete.

Những thay đổi/bổ sung/sửa đổi nào làm cho hệ thống kiểu của Scala trở nên hoàn thiện hơn so với các thuật toán và hệ thống chính thức?

+4

Có các liên kết/tham chiếu? (Đối với khán giả, như tôi :-) –

+7

Thực tế là hệ thống F là mạnh mẽ bình thường ngụ ý rằng hệ thống F không phải là Turing hoàn thành. Nó không ngụ ý rằng hệ thống kiểu của nó thì không. Và trong thực tế nó đã được chứng minh rằng [typechecking một hệ thống không bị hạn chế F là undecidable] (http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.6.6483) – sepp2k

+0

@ sepp2k - yikes, các điều tồi tệ nhất về Turing-đầy đủ và nó đã có điều đó. – Malvolio

Trả lời

4

Đây không phải là câu trả lời toàn diện nhưng lý do là bạn có thể xác định đệ quy loại.

Tôi đã hỏi các câu hỏi tương tự trước đây (about what a non-Turing complete language might look like). Các câu trả lời có dạng: một ngôn ngữ hoàn chỉnh Turing phải hỗ trợ hoặc lặp lại tùy ý hoặc đệ quy. Hệ thống kiểu Scala hỗ trợ sau

+3

Đệ quy các kiểu tồn tại trong hầu hết các ngôn ngữ, bao gồm Java và Pascal. Bất kỳ loại nào đề cập đến chính nó (như một danh sách liên kết) đều đệ quy. Bạn cần một cách để thực hiện tính toán ở cấp loại, chẳng hạn như ứng dụng kiểu. Trong Scala, bạn có kiểu thành viên và ứng dụng kiểu từng phần trong các bí danh kiểu. –

+2

Tôi có nghĩa là các loại đệ quy theo nghĩa của mã hóa peano: http://apocalisp.wordpress.com/2010/06/08/type-level-programming-in-scala/ sử dụng 'type', không phải' class' hoặc ' trait'. Tôi nghĩ điều đó khá rõ ràng trong bối cảnh. Như tôi đã nói, tôi đang vang vọng ở đây, những gì tôi đã được kể về sự hoàn thiện. –

+1

[Loại đệ quy] (http://en.wikipedia.org/wiki/Recursive_data_type) có thể được sử dụng để mã hóa các số như bạn nói, nhưng chúng không đủ để hoàn thành Turing. Những gì bạn muốn là một cách để tính toán, trong trường hợp này sử dụng ứng dụng kiểu (mà lần lượt sử dụng thay thế). Các thành viên kiểu Scala làm cho nó hơi dễ dàng, mặc dù Java thực hiện các thay thế tương tự cho Generics. –