Các giới hạn của hệ thống kiểm tra loại và loại là gì?

Question

Các hệ thống kiểu thường bị chỉ trích, vì bị hạn chế, đó là hạn chế ngôn ngữ lập trình và cấm các lập trình viên viết các chương trình thú vị.

Chris Smith claims:

Chúng tôi nhận được sự đảm bảo rằng chương trình là đúng (trong các thuộc tính kiểm tra bằng kiểm tra kiểu này), nhưng đến lượt chúng ta phải từ chối một số chương trình hấp dẫn.

và

Bên cạnh đó, có một chứng minh toán học bọc thép rằng một loại kiểm tra của bất kỳ lợi ích nào cả phải lúc nào cũng bảo thủ. Xây dựng trình kiểm tra loại không từ chối bất kỳ chương trình chính xác nào không chỉ khó khăn; điều đó là không thể.

Ai đó có thể phác thảo những chương trình thú vị này có thể là gì? Ở đâu nó được chứng minh rằng kiểm tra loại phải bảo thủ?

Và tổng quát hơn: Giới hạn của hệ thống kiểm tra loại và loại là gì?

Answer 1

Mọi người đã phát hiện ra rằng nếu bạn viết bài kiểm tra đầu tiên theo cách thực sự TDD, kiểm tra của bạn thường làm tốt hơn trong việc xác minh tính đúng đắn hơn hệ thống kiểm tra loại nghiêm ngặt. Vì vậy, để đo tính chính xác, một hệ thống kiểu mạnh không thực sự đo lường được.

Nhập mạnh mẽ thường có thể mua cho bạn một số tốc độ vì trình biên dịch có thể dễ dàng sử dụng kiểu gốc thay vì phải thực hiện kiểm tra kiểu khi chạy. Trường hợp tại điểm: nếu bạn đang thực hiện rất nhiều phép toán số nguyên, bạn sẽ thấy việc triển khai gõ mạnh mẽ có thể sẽ vượt quá khả năng nhập sai, vì các số liệu của bạn thường có thể được CPU sử dụng ngay và không cần phải được xác minh khi chạy.

Chương trình "thú vị"? Chắc chắn rồi. Thật dễ dàng để viết các tiện ích mở rộng của ngôn ngữ động. Ngoài ra, trong các hệ thống phân tán, nó có thể thực sự thuận tiện để có giao diện người dùng được đánh máy yếu và không phải tạo các đối tượng truyền dữ liệu cụ thể. Ví dụ, nếu bạn đã có một giao diện người dùng JavaScript và một phần phụ trợ C#, bạn có thể sử dụng LINQ trên đầu C# để tạo các lớp ẩn danh và gửi chúng tới Javascript của bạn thông qua JSON. Từ lớp JS, bạn chỉ có thể sử dụng các kiểu ẩn danh đó như thể chúng là các đối tượng hạng nhất và không phải trải qua nỗi đau khi mã hóa tất cả các hợp đồng dữ liệu của bạn một cách rõ ràng.

Answer 2

Bạn có thể diễn đạt mọi thứ bằng cả ngôn ngữ tĩnh và động. Bằng chứng == bạn có thể viết bất kỳ trình biên dịch ngôn ngữ nào trong bất kỳ ngôn ngữ hoàn chỉnh nào. Vì vậy, bất kể ngôn ngữ là gì, bạn có thể tạo ngôn ngữ tĩnh có X.

Điều gì có thể thú vị khi gõ động? ... Với kiểu gõ đủ tốt, bạn có thể tương tác với các đối tượng qua mạng mà không hề biết vượt qua kết quả của họ (của một loại không rõ cho bạn) như các tham số cho các hàm cục bộ mà thực sự có thể làm một cái gì đó hữu ích.

Câu trả lời tĩnh cho vấn đề đó sẽ là bọc mọi thứ trong "giao diện có thể xuất" cung cấp .call() và .provides?() Làm việc trên tên văn bản, nhưng điều đó chắc chắn sẽ khó hơn.

Đó là trường hợp "hạn chế" nhất mà tôi biết và nó thực sự kéo dài mọi thứ một chút (chỉ thực sự hữu ích với các đối tượng giả?). Đối với giới hạn lý thuyết, không có gì - bạn chỉ cần thêm một số mã để khắc phục các vấn đề thực tế.

Answer 3

Thật khó để tìm ra các so sánh thực dụng khách quan về các vấn đề nhập tĩnh hoặc động vì nó thường là một cuộc chiến tôn giáo. Các tóm tắt tóm tắt nhỏ mà bạn đã trích dẫn có xu hướng giống như tuyên bố từ chối trách nhiệm everone làm cho rằng dường như là 'chấp nhận' cho tất cả mọi người những ngày này.

Là người có kinh nghiệm chủ yếu là ngôn ngữ được nhập tĩnh, tôi đã cố gắng hiểu một số sự cân bằng trong chuỗi blog trong khi quay lại. Rất nhiều hãy cẩn thận, nhưng bạn có thể kiểm tra nửa sau của this blog entry để so sánh một số gợi ý là câu trả lời cho câu hỏi của bạn.

Dưới đây là một trích đoạn mà thấy một cửa sổ vào thương mại-off:

Trong một nghĩa nào đó, chức năng nhỏ này nắm bắt được bản chất của cuộc tranh luận đang diễn ra giữa tĩnh và động gõ. Các lập trình viên có thể tạo loại tĩnh miền cụ thể để cấu trúc chương trình, truyền đạt ý định, và loại trừ một lớp các lỗi và hành vi tại thời gian biên dịch, với mức giá vì phải tác giả rằng cấu trúc và trung gian cấu trúc mismatches tại ranh giới mô-đun. Hoặc các lập trình viên có thể chọn để tính toán tất cả mọi thứ nhất chỉ với vô hướng và danh sách, trong trường hợp dữ liệu chảy dễ dàng ở khắp mọi nơi, kết quả là mã ngắn, nhưng với sự mất mát của thời gian biên dịch kiểm tra và vận chuyển về ý định.

và ví dụ đang chạy hiển thị trường hợp chương trình gõ tĩnh không cho phép hành vi hữu ích/thú vị theo bản chất của nó.

Answer 4

Tôi nghĩ rằng an eval function có thể hữu ích đôi khi, nhưng không bao giờ cần thiết (nó không phổ biến cho một ngôn ngữ gõ tĩnh, xem giải thích trên liên kết).

Answer 5

Dưới đây là một ví dụ đơn giản (bằng Python, nhưng hoàn toàn không liên quan đến các vấn đề gõ của nó):

# The company deals with rectangles. They have horizontal and vertical lengths 
# that should not be mixed. Programmer A writes: 

class Rectange: 
    def __init__(self, width, height): 
     enforce_type('horizontal', width) 
     enforce_type('vertical', height) 
     # 
     # A: Hehe! I'm so smart! With my patented type system if I try to 
     # write "width * width" I'll have a loud error so I'll know I'm wrong. 
     # 
     area = width * height 
     enforce_type('square_meters', area) 
     ... 

# Everyone's happy. The company shows off A's type system on the conference. 

... 

# Much later, the clients request ability to specify square by entering only 
# one length. Programmer B writes: 

class Square(Rectangle): 
    def __init__(self, width): 
     Rectange.__init__(self, width, width) 
     # !! 
     # Error happens! 'horizontal' is not 'vertical'! 
     # 
     # B: Dear Management, I would like to request a weeklong leave since I 
     # have to track Programmer A's house and either talk him into changing 
     # his patented type system or BEAT HIM WITH MY LAPTOP until he agrees. 
     # 

Nó rất khó để tạo ra một hệ thống kiểu đó sẽ thấy trước bất kỳ loại ngoại lệ có thể từ các quy tắc, đặc biệt là nếu bạn đang tạo khung cơ sở sẽ được mọi người sử dụng sau này.

Để trả lời câu hỏi trực tiếp của bạn, bạn đang ở bên nào: Lập trình viên A hoặc Lập trình viên B?

Answer 6

Một ví dụ thú vị là This Paper, có lẽ chỉ là so sánh táo-to-táo từng được thực hiện trên kiểu nhập tĩnh so với động. Họ thực hiện tự (một ngôn ngữ như smalltalk, nhưng với nguyên mẫu thay vì các lớp học) với cả suy luận kiểu (tĩnh) và kiểu phản hồi (động).

Kết quả thú vị nhất là động cơ suy luận loại có rất nhiều sự cố khi giải quyết giữa các số nguyên máy và số nguyên chính xác tùy ý - Chúng tự động quảng bá trong chế độ tự vani và do đó không thể phân biệt bằng hệ thống kiểu có nghĩa là trình biên dịch phải bao gồm mã để quảng bá cho BigInt trên mọi hoạt động số nguyên.

Chúng chạy ngược với giới hạn của hệ thống loại: Không thể kiểm tra giá trị thực của số nguyên.

Tôi nghĩ rằng không có giới hạn lý thuyết để loại hệ thống nói chung, nhưng bất kỳ trình kiểm tra loại nhất định chỉ có thể xử lý một hệ thống loại giới hạn cụ thể và sẽ có các chương trình không thể xác định được những gì đang diễn ra. Vì trình tự inferencer kiểu tự cho phép cho các tập hợp các kiểu, nó đơn giản biên dịch cả hai đường dẫn. Trình kiểm tra loại yêu cầu hội tụ trên một loại đơn lẻ sẽ phải từ chối chương trình. (Mặc dù nó có lẽ sẽ có mã đặc biệt cho trường hợp này.)

Answer 7

Tôi không chắc chắn nhưng tôi tin rằng các vấn đề bạn đang đề cập đến là với Hệ thống loại đại số như Haskell và ML. Các ngôn ngữ này cố gắng thực hiện phân tích "tĩnh" hoàn chỉnh trước khi bạn chạy chương trình.

Một số phiền toái thú vị với phân tích tĩnh rất nghiêm ngặt trong hệ thống loại đại số là rất khó để có một thùng chứa chứa hỗn hợp các đối tượng thuộc các loại khác nhau.

Ví dụ: trong hầu hết các ngôn ngữ chính thống, bạn có thể có một hỗn hợp không đồng nhất của các loại trong danh sách. Một ví dụ trong python sẽ là:

["a",1,"b",2] 

Để làm điều này trong một hệ thống loại nghiêm ngặt, bạn sẽ phải làm một loại hợp nhất và mẫu phù hợp với tất cả các loại có thể.

Nhưng điều thú vị thực sự thiếu trong ngôn ngữ là sự quan tâm mạnh mẽ mà bạn có trong ngôn ngữ hiện đại nhất (ví dụ: C#, Java, Python, Ruby, Lisp).

Do đó, các ngôn ngữ này cho phép bạn thực hiện một số chương trình meta và ràng buộc dữ liệu mạnh mẽ mà bạn không thể thực hiện với phân tích tĩnh hoàn chỉnh.

Answer 8

Có rất nhiều ví dụ phức tạp, nhưng dường như hầu hết mọi người đều bỏ lỡ ví dụ tầm thường.

Đây là chương trình python chính xác trả lời câu hỏi về giá trị tuyệt đối của 5 và -5 là gì.

def abs(x): 
    def signum(f): 
     if f > 0: 
      return 1 
     else: 
      return "non-positive" 
    if signum(x) == 1: 
     return x 
    else: 
     return -x 

print("abs(5) = %r and abs(-5) = %r" % (abs(5), abs(-5))) 

Rõ ràng là abs và signum mất int làm tham số; abs luôn trả về int, nhưng signum có thể trả về int hoặc string. Bây giờ, nếu chúng tôi giới thiệu một trình kiểm tra kiểu (nhưng không phải bất kỳ trình kiểm tra kiểu nào; trình kiểm tra kiểu của scala sẽ chỉ nói "signum là int->Any"!) Thì chương trình này sẽ bị từ chối ... tuy nhiên, nó là chính xác và sẽ không bao giờ gặp sự cố mạnh mẽ-loại-conformance là lý do tai nạn.

Answer 9

SpeC# có hệ thống kiểu không có loại rỗng và an toàn tĩnh. (http://research.microsoft.com/en-us/projects/specsharp/)

Answer 10

Giới hạn của hệ thống kiểm tra loại và loại là gì?

Tôi sẽ giả định rằng "hệ thống kiểu" ngụ ý một ngôn ngữ lập trình được nhập tĩnh.

Nhập tĩnh nghĩa là các loại được chọn tại thời gian biên dịch. Giới hạn ở đây là trình biên dịch chỉ có thể tối ưu hóa dựa trên thông tin có sẵn tại thời gian biên dịch. Điều này có thể được coi là một hạn chế. Trong các ngôn ngữ lập trình được nhập động, người thông dịch có thể phân tích và tối ưu hóa chương trình khi chạy. Điều này có nghĩa là nó có thể tối ưu hóa dựa trên các mẫu sử dụng.

Answer 11

Tôi nghĩ câu đầu tiên về mặt kỹ thuật là sai, mặc dù thực tế là đúng.

Nhập tĩnh cơ bản giống như chứng minh các thuộc tính của chương trình và bằng cách sử dụng một logic đủ mạnh, bạn có thể chứng minh rằng tất cả các chương trình thú vị đều chính xác.

Vấn đề là đối với suy luận kiểu logic mạnh mẽ không còn hoạt động nữa và bạn phải cung cấp bằng chứng như một phần của chương trình để trình kiểm tra loại có thể thực hiện công việc của mình. Một ví dụ cụ thể là những người đặt hàng cao cấp hơn như Coq. Coq sử dụng một logic cực kỳ mạnh mẽ, nhưng nó cũng vô cùng tẻ nhạt để có được bất cứ điều gì được thực hiện trong Coq, bởi vì bạn phải cung cấp bằng chứng rất chi tiết.

Các loại chương trình thú vị sẽ mang đến cho bạn nhiều rắc rối nhất sẽ là phiên dịch, vì hành vi của họ phụ thuộc hoàn toàn vào đầu vào. Về cơ bản, bạn sẽ cần phải chứng minh một cách phản ánh tính chính xác của việc kiểm tra kiểu cho đầu vào đó.

Đối với tuyên bố thứ hai, ông có thể đề cập đến định lý không hoàn hảo của Gödels. Nó nói rằng đối với bất kỳ hệ thống chứng minh nào có các báo cáo thực sự về số học (logic cộng và nhân các số tự nhiên) không thể được chứng minh trong hệ thống chứng minh. Được dịch sang các hệ thống kiểu tĩnh, bạn sẽ có một chương trình không làm bất cứ điều gì xấu nhưng hệ thống kiểu tĩnh không thể chứng minh điều đó.

Các mẫu đối sánh này được xây dựng bằng cách tham chiếu trở lại định nghĩa của hệ thống chứng minh, nói về cơ bản "Tôi không thể được chứng minh" được dịch thành số học, điều này không thú vị lắm. IMHO một chương trình được xây dựng tương tự sẽ không thú vị.

Answer 12

Nếu bạn xem Mitchell's book Concepts in Programming Languages tr.134, bạn sẽ tìm thấy một số chi tiết về những gì được gọi là "Tính bảo thủ của thời gian biên dịch kiểm tra". Vấn đề là một số tính năng "thú vị" như truy cập out-of-bounds cho mảng không thể được kiểm tra tĩnh, vì họ sẽ yêu cầu đánh giá của chương trình/mọi chương trình có thể chạy. Kết quả undecidability tiêu chuẩn cho bạn biết rằng bạn phải giải quyết vấn đề Halting để thực sự kiểm tra truy cập mảng MỌI.

Answer 13

Tôi nghĩ rằng có một sự hiểu lầm. Đúng là bất kỳ hệ thống kiểu nào sẽ từ chối một chương trình chính xác (tôi không nhớ tên chính xác của kết quả, vì vậy tôi không thể tra cứu nó ngay bây giờ, xin lỗi). Cũng đúng là bất kỳ ngôn ngữ hoàn chỉnh nào của Turing cũng có thể làm giống như bất kỳ ngôn ngữ nào khác, do đó, nó là sai lầm rằng có một số chương trình trong các ngôn ngữ được gõ động mà bạn không thể sao chép, trong Haskell.

Bắt là thực tế là một hệ thống loại sẽ từ chối một chương trình không có nghĩa là nó sẽ từ chối tất cả các chương trình tương đương với nó. Vì vậy, một số chương trình sẽ bị từ chối, nhưng bạn có thể thay thế chúng bằng các chương trình khác, tương đương. Như một ví dụ uống theo chương trình Scala sau

def foo: Int = 
    if (1 > 0) 15 else "never happens" 

Trình kiểm tra loại sẽ từ chối nó, như sự biểu hiện if (1 > 0) 15 else "never happens" là chính thức loại Any. Khi bạn chạy nó, nó chắc chắn sẽ trả về một số nguyên, nhưng không đánh giá 1 > 0 bạn không thể chắc chắn rằng nó sẽ không trả về một chuỗi. Bạn có thể viết, bằng Python

def foo(): 
    if 1 > 0: 
    return 15 
    else: 
    return "never happens" 

và trình biên dịch Python sẽ không quan tâm.

Tất nhiên có những chương trình tương đương với trang này bạn có thể viết trong Scala, đơn giản nhất là

def foo: Int = 15