Skip to content

Instantly share code, notes, and snippets.

@gavinwahl
Last active August 29, 2015 14:25
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save gavinwahl/8fc0f84bfdd990aac42d to your computer and use it in GitHub Desktop.
Save gavinwahl/8fc0f84bfdd990aac42d to your computer and use it in GitHub Desktop.
'Dynamically' typed pipelines of composed functions
{-# 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