Gõ chữ GADTs

Question

Giả sử tôi đang viết một DSL và muốn hỗ trợ cả hỗ trợ kiểu ma và các biểu thức được nhập sai. các loại giá trị của tôi có thể

{-# LANGUAGE GADTs, DataKinds #-} 

data Ty = Num | Bool deriving (Typeable) 

data Val a where 
    VNum :: Int -> Val Num 
    VBool :: Bool -> Val Bool 

và tôi có thể làm việc với một phantom xóa phiên bản

{-# LANGUAGE ExistentialQuantification #-} 

data Valunk = forall a . Valunk (V' a) 

Bây giờ, tôi có thể hoạt động trên các giá trị của Valunk bởi case ing ra cả VNum và VBool và thậm chí thiết lập lại phantom của tôi các loại theo cách này

getNum :: Valunk -> Maybe (Val Num) 
getNum (Valunk n@(VNum _)) = Just n 
getNum _     = Nothing 

Nhưng điều này chỉ cảm thấy như tôi đang thực hiện lại Typeable máy móc. Thật không may, GHC sẽ không cho phép tôi lấy được một Typeable cho Val

src/Types/Core.hs:97:13: 
    Can't make a derived instance of `Typeable (Val a)': 
     Val must only have arguments of kind `*' 
    In the data declaration for Val 

Có cách nào để có được xung quanh hạn chế này? Tôi rất muốn viết

getIt :: Typeable a => Valunk -> Maybe (Val a) 
getIt (Valunk v) = cast v 

nhưng ngay bây giờ tôi phải dùng đến máy móc như thế này

class Typeably b x where kast :: x a -> Maybe (x b) 
instance Typeably Num Val where 
    kast n@(VNum _) = Just n 
    kast _   = Nothing 

cho tất cả các loại của tôi.

Answer 1

Bạn có thể lấy được Data.Typeable trên của riêng bạn:

{-# LANGUAGE GADTs, DataKinds, DeriveDataTypeable, ExistentialQuantification #-} 

import Data.Typeable 

data Ty = TNum | TBool deriving Typeable 

data Valunk = forall a. Typeable a => Valunk a 

data Val a where 
    VInt :: Int -> Val TNum 
    VBool :: Bool -> Val TBool 

instance Show (Val a) where 
    show (VInt a) = show a 
    show (VBool a) = show a 

valtypenam = mkTyCon3 "package" "module" "Val" 

instance Typeable (Val a) where 
    typeOf _ = mkTyConApp valtypenam [] 

getIt :: Valunk -> Maybe (Val a) 
getIt (Valunk p) = cast p 

này sẽ cung cấp các chức năng nhận được nó. Chỉ cần chắc chắn để đặt tên cho loại của bạn một cách chính xác (do đó tập tin các gói, mô-đun và loại trung thực) nếu không các gói khác có thể nhận được vào vấn đề.

Để biết thêm một số ví dụ về cách viết các trường hợp này, hãy xem: Data.Derive.Typeable source.

EDIT: Tôi đã có một bản sao rất lạ và lỗi quá khứ trong mã, nhưng bây giờ nó hoạt động.

Answer 2

Trước hết, bạn cần lưu trữ một nhân chứng rằng các loại định lượng trong Valunk là trong Typeable:

data Valunk = forall a . Typeable a => Valunk (Val a) 

Khi bạn có điều này, bạn chỉ có thể sử dụng gcast để đạt được những gì bạn đang yêu cầu cho:

getIt :: Typeable a => Valunk -> Maybe (Val a) 
getIt (Valunk v) = gcast v 

này đã được thử nghiệm với:

data Val a where 
    VNum :: Int -> Val Int 
    VBool :: Bool -> Val Bool