Last active
August 29, 2015 14:25
-
-
Save gavinwahl/8fc0f84bfdd990aac42d to your computer and use it in GitHub Desktop.
'Dynamically' typed pipelines of composed functions
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE GADTs, ExistentialQuantification, TypeOperators, StandaloneDeriving #-} | |
import Data.Type.Equality | |
import Text.Read | |
data Renderer a b where | |
-- Lifts a normal function to a Renderer. The String is just a label | |
-- to see what's going on. | |
Lift :: String -> (a -> b) -> Renderer a b | |
-- composes two Renderers | |
Compose :: Renderer a b -> Renderer b c -> Renderer a c | |
-- Term-level representations of the types we're interested in | |
data Type a where | |
TInt :: Type Int | |
TBool :: Type Bool | |
TStr :: Type String | |
-- Packages a Renderer with term-level witnesses of its type, to pattern | |
-- match on. | |
data ERender = forall a b. ERender (Type a) (Type b) (Renderer a b) | |
-- Show instances just to see what's going on | |
instance Show (Renderer a b) where | |
show (Lift name _) = "(Lift \"" ++ name ++ "\" _)" | |
show (Compose a b) = "Compose (" ++ show a ++ ", " ++ show b ++ ")" | |
deriving instance (Show (Type a)) | |
deriving instance (Show ERender) | |
-- takes two Types and returns an equality proof, if it exists. | |
typeEq :: Type a -> Type b -> Maybe (a :~: b) | |
typeEq TInt TInt = Just Refl | |
typeEq TBool TBool = Just Refl | |
typeEq TStr TStr = Just Refl | |
typeEq _ _ = Nothing | |
-- A lookup table of primitives. It could just as easily | |
-- be a `Map String ERender` | |
lookupRenderer :: String -> Maybe ERender | |
lookupRenderer "intToStr" = Just $ ERender TInt TStr (Lift "intToStr" show) | |
lookupRenderer "intToBool" = Just $ ERender TInt TBool (Lift "intToBool" (0 ==)) | |
lookupRenderer "boolToStr" = Just $ ERender TBool TStr (Lift "boolToStr" show) | |
lookupRenderer "strToBool" = Just $ ERender TStr TBool (Lift "strToBool" ("12" ==)) | |
lookupRenderer _ = Nothing | |
typecheck :: [String] -> Maybe ERender | |
typecheck [] = Nothing | |
typecheck [x] = lookupRenderer x | |
typecheck (x:xs) = do | |
(ERender x_i x_o x') <- lookupRenderer x | |
(ERender xs_i xs_o xs') <- typecheck xs | |
-- This pattern match will fail and result in Nothing (the input | |
-- list is invalid) if the input type of xs doesn't match the output | |
-- type of x. Otherwise, we have a proof that they match and we can | |
-- compose them. | |
Refl <- typeEq x_o xs_i | |
return $ ERender x_i xs_o (Compose x' xs') | |
runRenderer :: Renderer a b -> a -> b | |
runRenderer (Lift _ f) = f | |
runRenderer (Compose a b) = runRenderer b . runRenderer a | |
example :: Maybe String | |
example = do | |
(ERender TInt TStr pipeline) <- typecheck ["intToStr", "strToBool", "boolToStr"] | |
-- we (and the compiler) are now certain that `pipeline :: Renderer Int String` | |
-- and so can call it without any Maybes. | |
return $ runRenderer pipeline 123 | |
typecheckInteractive :: IO () | |
typecheckInteractive = do | |
putStr "enter pipeline as list: " | |
line <- getLine | |
case readMaybe line of | |
Nothing -> putStrLn "Syntax error, please enter a list of strings" | |
(Just ops) -> | |
case typecheck ops of | |
Nothing -> putStrLn "Couldn't typecheck" | |
Just (ERender a b _) -> putStrLn $ "That's a pipeline from " ++ (show a) ++ " to " ++ (show b) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment