Dữ liệu ... có nghĩa là gì trong Haskell?

Question

tôi thấy đoạn này tại the devlog of omegagb:

data ExecutionAST result where 
    Return :: result -> ExecutionAST result 
    Bind :: (ExecutionAST oldres) -> (oldres -> ExecutionAST result) -> 
      ExecutionAST result 
    WriteRegister :: M_Register -> Word8 -> ExecutionAST() 
    ReadRegister :: M_Register -> ExecutionAST Word8 
    WriteRegister2 :: M_Register2 -> Word16 -> ExecutionAST() 
    ReadRegister2 :: M_Register2 -> ExecutionAST Word16 
    WriteMemory :: Word16 -> Word8 -> ExecutionAST() 
    ReadMemory :: Word16 -> ExecutionAST Word8 

nào data ... where nghĩa là gì? Tôi nghĩ từ khóa data được sử dụng để xác định loại mới.

Answer 1

Định nghĩa loại mới, cú pháp được gọi là generalized algebraic data type.

Tổng quát hơn cú pháp thông thường. Bạn có thể viết bất kỳ định nghĩa kiểu bình thường (ADT) sử dụng GADTs:

data E a = A a | B Integer 

có thể được viết như sau:

data E a where 
    A :: a -> E a 
    B :: Integer -> E a 

Nhưng bạn cũng có thể hạn chế những gì trên phía bên tay phải:

data E a where 
    A :: a -> E a 
    B :: Integer -> E a 
    C :: Bool -> E Bool 

không thể thực hiện với khai báo ADT thông thường.

Để biết thêm, hãy kiểm tra Haskell wiki hoặc this video.

---

Lý do là loại an toàn. ExecutionAST t được cho là loại báo cáo trả về t. Nếu bạn viết một ADT bình thường

data ExecutionAST result = Return result 
         | WriteRegister M_Register Word8 
         | ReadRegister M_Register 
         | ReadMemory Word16 
         | WriteMemory Word16 
         | ... 

sau đó ReadMemory 5 sẽ là một giá trị đa hình kiểu ExecutionAST t, thay vì monomorphic ExecutionAST Word8, và điều này sẽ gõ kiểm tra:

x :: M_Register2 
x = ... 

a = Bind (ReadMemory 1) (WriteRegister2 x) 

tuyên bố đó sẽ đọc bộ nhớ từ vị trí 1 và viết thư để đăng ký x. Tuy nhiên, việc đọc từ bộ nhớ cho các từ 8 bit và ghi vào x yêu cầu các từ 16 bit. Bằng cách sử dụng GADT, bạn có thể chắc chắn điều này sẽ không biên dịch. Các lỗi biên dịch thời gian tốt hơn các lỗi thời gian chạy.

GADT cũng bao gồm existential types. Nếu bạn cố gắng viết liên kết theo cách này:

data ExecutionAST result = ... 
          | Bind (ExecutionAST oldres) 
            (oldres -> ExecutionAST result) 

thì nó sẽ không biên dịch từ "oldres" không có trong phạm vi, bạn phải viết:

data ExecutionAST result = ... 
          | forall oldres. Bind (ExecutionAST oldres) 
               (oldres -> ExecutionAST result) 

Nếu bạn đang bối rối, kiểm tra video được liên kết cho ví dụ đơn giản, có liên quan.

Answer 2

Lưu ý rằng nó cũng có thể đặt chế lớp:

data E a where 
    A :: Eq b => b -> E b