cách phân tích chuỗi thành cây cú pháp bằng GADT

Question

Tôi đã đọc phần giới thiệu GADT here và tôi đã tìm thấy ý tưởng hạn chế lập trình để tạo đúng loại cây cú pháp tuyệt vời và tôi đưa ý tưởng này vào trình thông dịch tính toán lambda đơn giản của tôi, sau đó tôi nhận ra rằng tôi không thể phân tích một chuỗi thành cây cú pháp này, bởi vì một hàm phân tích cú pháp cần phải trả về các kiểu cây cú pháp khác nhau, tùy thuộc vào đầu vào. Dưới đây là một ví dụ:

{-# LANGUAGE GADTs #-} 
data Ident 
data Lambda 
data Application 

data Expr a where 
    Ident :: String -> Expr Ident 
    Lambda :: Expr Ident -> Expr a -> Expr Lambda 
    Application :: Expr a -> Expr a -> Expr Application 

Trước khi sử dụng GADTs, tôi đã sử dụng này:

data Expr = Lambda Expr Expr 
      | Ident String 
      | Application Expr Expr 

GADTs là lợi thế lớn ở đây, bacuse bây giờ tôi không thể tạo cây cú pháp không hợp lệ như Lambda (Application ..) ...

Nhưng với GADT, tôi không thể phân tích cú pháp chuỗi và tạo cây phân tích cú pháp. Dưới đây là phân tích cú pháp cho Lambda, ident, và các biểu thức Ứng dụng:

ident :: Parser (Expr Ident) 
ident = ... 

lambda :: Parser (Expr Lambda) 
lambda = ... 

application :: Parser (Expr Application) 
application = ... 

Bây giờ vấn đề là:

expr = choice [ident, application, lambda] 

Điều này rõ ràng không hoạt động, vì mỗi phân tích cú pháp đang trở lại loại khác nhau.

Vì vậy, có cách nào để phân tích chuỗi và tạo cây cú pháp, với GADT không?

Answer 1

Bạn có thể sử dụng GADT để tạo loại có chứa Expr a đối với một số không rõ a.

data AnyExpr where AnyExpr :: Expr a -> AnyExpr 

Trong tình huống mà bạn không muốn hạn chế Expr đến một loại hình cụ thể, sử dụng AnyExpr.

anyExpr :: Parser (Expr a) -> Parser AnyExpr 
anyExpr p = fmap AnyExpr p 

expr :: Parser AnyExpr 
expr = choice [anyExpr ident, anyExpr application, anyExpr lambda]