Tôi làm cách nào để khôi phục tính năng chia sẻ trong GADT?

Question

Trong Type-Safe Observable Sharing in Haskell Andy Gill cho thấy cách khôi phục chia sẻ tồn tại trên cấp độ Haskell, trong DSL. Giải pháp của ông được thực hiện trong data-reify package. Cách tiếp cận này có thể được sửa đổi để làm việc với GADT không? Ví dụ, cho GADT này:

data Ast e where 
    IntLit :: Int -> Ast Int 
    Add :: Ast Int -> Ast Int -> Ast Int 
    BoolLit :: Bool -> Ast Bool 
    IfThenElse :: Ast Bool -> Ast e -> Ast e -> Ast e 

Tôi muốn phục hồi chia sẻ bằng cách chuyển đổi các AST trên để

type Name = Unique 

data Ast2 e where 
    IntLit2 :: Int -> Ast2 Int 
    Add2 :: Ast2 Int -> Ast2 Int -> Ast2 Int 
    BoolLit2 :: Bool -> Ast2 Bool 
    IfThenElse2 :: Ast2 Bool -> Ast2 e -> Ast2 e -> Ast2 e 
    Var :: Name -> Ast2 e 

bằng cách của một hàm

recoverSharing :: Ast -> (Map Name, Ast2 e1, Ast2 e2) 

(Tôi m không chắc chắn về loại recoverSharing.)

Lưu ý rằng tôi không quan tâm đến việc giới thiệu bindin mới gs thông qua một cấu trúc let, nhưng chỉ trong việc khôi phục chia sẻ tồn tại trên cấp độ Haskell. Đó là lý do tại sao tôi có recoverSharing trả lại số Map.

Nếu nó không thể được thực hiện như gói tái sử dụng, ít nhất nó có thể được thực hiện cho GADT cụ thể không?

Answer 1

Câu đố thú vị! Hóa ra bạn có thể sử dụng dữ liệu-reify với GADTs. Những gì bạn cần là một wrapper ẩn các loại trong một existential. Loại sau này có thể được truy lục bằng cách khớp mẫu trên loại dữ liệu Type.

data Type a where 
    Bool :: Type Bool 
    Int :: Type Int 

data WrappedAst s where 
    Wrap :: Type e -> Ast2 e s -> WrappedAst s 

instance MuRef (Ast e) where 
    type DeRef (Ast e) = WrappedAst 
    mapDeRef f e = Wrap (getType e) <$> mapDeRef' f e 
    where 
     mapDeRef' :: Applicative f => (forall b. (MuRef b, WrappedAst ~ DeRef b) => b -> f u) -> Ast e -> f (Ast2 e u) 
     mapDeRef' f (IntLit i) = pure $ IntLit2 i 
     mapDeRef' f (Add a b) = Add2 <$> (Var Int <$> f a) <*> (Var Int <$> f b) 
     mapDeRef' f (BoolLit b) = pure $ BoolLit2 b 
     mapDeRef' f (IfThenElse b t e) = IfThenElse2 <$> (Var Bool <$> f b) <*> (Var (getType t) <$> f t) <*> (Var (getType e) <$> f e) 

getVar :: Map Name (WrappedAst Name) -> Type e -> Name -> Maybe (Ast2 e Name) 
getVar m t n = case m ! n of Wrap t' e -> (\Refl -> e) <$> typeEq t t' 

Dưới đây là toàn bộ mã: https://gist.github.com/3590197

Edit: Tôi thích sử dụng Typeable trong câu trả lời khác. Vì vậy, tôi đã thực hiện phiên bản mã của mình với Typeable cũng vậy: https://gist.github.com/3593585. Mã ngắn hơn đáng kể. Type e -> được thay thế bằng Typeable e =>, cũng có một nhược điểm: chúng tôi không còn biết rằng các loại có thể bị giới hạn ở Int và Bool, điều này có nghĩa là phải có giới hạn Typeable e trong IfThenElse.

Answer 2

Tôi sẽ cố gắng cho thấy rằng điều này có thể được thực hiện cho các GADT cụ thể, sử dụng GADT làm ví dụ.

Tôi sẽ sử dụng gói Data.Reify. Điều này đòi hỏi tôi phải xác định một cấu trúc dữ liệu mới, trong đó các vị trí recusive được thay thế bởi một tham số.

data AstNode s where 
    IntLitN :: Int -> AstNode s 
    AddN :: s -> s -> AstNode s 
    BoolLitN :: Bool -> AstNode s 
    IfThenElseN :: TypeRep -> s -> s -> s -> AstNode s 

Lưu ý rằng tôi xóa rất nhiều thông tin loại có sẵn trong GADT gốc. Đối với ba hàm tạo đầu tiên, rõ ràng loại liên kết là gì (Int, Int và Bool). Đối với người cuối cùng tôi sẽ nhớ loại sử dụng TypeRep (có sẵn trong Data.Typeable). Ví dụ cho MuRef, theo yêu cầu của gói thống nhất, được hiển thị bên dưới.

instance Typeable e => MuRef (Ast e) where 
    type DeRef (Ast e)  = AstNode 
    mapDeRef f (IntLit a) = pure $ IntLitN a 
    mapDeRef f (Add a b) = AddN <$> f a <*> f b 
    mapDeRef f (BoolLit a) = pure $ BoolLitN a 
    mapDeRef f (IfThenElse a b c :: Ast e) = 
    IfThenElseN (typeOf (undefined::e)) <$> f a <*> f b <*> f c 

Bây giờ chúng tôi có thể sử dụng reifyGraph để khôi phục chia sẻ. Tuy nhiên, rất nhiều loại thông tin đã bị mất. Hãy thử phục hồi nó.Tôi thay đổi định nghĩa của bạn về Ast2 hơi:

data Ast2 e where 
    IntLit2 :: Int -> Ast2 Int 
    Add2 :: Unique -> Unique -> Ast2 Int 
    BoolLit2 :: Bool -> Ast2 Bool 
    IfThenElse2 :: Unique -> Unique -> Unique -> Ast2 e 

Đồ thị từ gói cụ thể hóa trông như thế này (nơi e = AstNode):

data Graph e = Graph [(Unique, e Unique)] Unique  

Cho phép tạo ra một cấu trúc dữ liệu đồ thị mới, nơi chúng tôi có thể lưu trữ Ast2 Int và Ast2 Bool riêng biệt (do đó, nơi thông tin về loại đã được khôi phục):

data Graph2 = Graph2 [(Unique, Ast2 Int)] [(Unique, Ast2 Bool)] Unique 
      deriving Show 

Bây giờ chúng ta chỉ cần tìm một hàm từ Graph AstNode (kết quả của reifyGraph) để Graph2:

recoverTypes :: Graph AstNode -> Graph2 
recoverTypes (Graph xs x) = Graph2 (catMaybes $ map (f toAst2Int) xs) 
            (catMaybes $ map (f toAst2Bool) xs) x where 
    f g (u,an) = do a2 <- g an 
        return (u,a2) 

    toAst2Int (IntLitN a) = Just $ IntLit2 a 
    toAst2Int (AddN a b) = Just $ Add2 a b 
    toAst2Int (IfThenElseN t a b c) | t == typeOf (undefined :: Int) 
         = Just $ IfThenElse2 a b c 
    toAst2Int _   = Nothing 

    toAst2Bool (BoolLitN a) = Just $ BoolLit2 a 
    toAst2Bool (IfThenElseN t a b c) | t == typeOf (undefined :: Bool) 
          = Just $ IfThenElse2 a b c 
    toAst2Bool _   = Nothing 

Cho phép làm một ví dụ:

expr = Add (IntLit 42) expr 

test = do 
    graph <- reifyGraph expr 
    print graph 
    print $ recoverTypes graph 

Bản in:

let [(1,AddN 2 1),(2,IntLitN 42)] in 1 
Graph2 [(1,Add2 2 1),(2,IntLit2 42)] [] 1 

Dòng đầu tiên cho chúng ta thấy rằng reifyGraph đã chia sẻ chính xác chia sẻ. Dòng thứ hai cho chúng ta thấy rằng chỉ có các loại Ast2 Int được tìm thấy (cũng đúng).

Phương pháp này có thể dễ dàng thích ứng với các GADT cụ thể khác, nhưng tôi không thấy nó có thể được làm hoàn toàn chung chung như thế nào.

Mã hoàn chỉnh có thể được tìm thấy tại http://pastebin.com/FwQNMDbs.