I was taking a quick look at Idris earlier and I find it quite interesting that a program like this works:
module Main
toType : String -> Type
toType "string" = String
toType "bool" = Bool
toType _ = ()
fromType : Type -> String
fromType String = "string"
fromType Bool = "bool"
fromType _ = "something else"
main : IO ()
main = do typeStr <- getLine
putStr (fromType (toType typeStr))