Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- {-# LANGUAGE ExistentialQuantification #-}
- {-# LANGUAGE GADTs #-}
- {-# LANGUAGE KindSignatures #-}
- {-# LANGUAGE ViewPatterns #-}
- module Things where
- -- Data
- data X = X String Bool Char
- -- What I get as input
- data Ty = STRING | BOOL | INT
- -- Representation of things I can pick out of the data.
- data Thing :: * -> * where
- TString :: Thing String
- TBool :: Thing Bool
- TInt :: Thing Char
- -- Existentialized version of Thing, witnesses the constraint that I'll need.
- data SomeThing
- = forall k. Show k => SomeThing (Thing k)
- -- A polymorphic structure
- data Foo a b = Foo a b deriving Show
- toSomeThing :: Ty -> SomeThing
- toSomeThing BOOL = SomeThing TBool
- toSomeThing INT = SomeThing TInt
- toSomeThing STRING = SomeThing TString
- -- dependently-typed extraction
- extractThing :: Thing a -> X -> a
- extractThing TString (X s b i) = s
- extractThing TBool (X s b i) = b
- extractThing TInt (X s b i) = i
- -- Extract various parts of something into a polymorphic structure
- extractThings :: Thing a -> Thing b -> X -> Foo a b
- extractThings ta tb x = Foo (extractThing ta x) (extractThing tb x)
- -- a "dependently typed" operation but returns a simple type
- doit :: (Show a, Show b) => Thing a -> Thing b -> X -> String
- doit ta tb = show . extractThings ta tb
- -- monomorphic signature version
- doitSimple :: Ty -> Ty -> X -> String
- doitSimple (toSomeThing -> SomeThing ta) (toSomeThing -> SomeThing tb) = doit ta tb
- -- But this doesn't work!
- --doitBad :: Ty -> Ty -> X -> String
- --doitBad a b = doit ta tb
- -- where
- -- (SomeThing ta) = toSomeThing a
- -- (SomeThing tb) = toSomeThing b
Add Comment
Please, Sign In to add comment