Haskell doesn't need macros, eh?

[pozorvlak]

A comparison of the Haskell argmunger with its Arc equivalent (or even its Perl equivalent) should make something clear. It's been claimed that Haskell doesn't need macros, because most of the things that Lispers need macros for can be done in Haskell using lazy evaluation and so on. But the argmunger example makes it clear that there are things

Comments

[ryani]

The proof drawback is pretty simple to explain.

Lets say you have a function

SprintfType :: String -> *
SprintfType ('%':'d':s) = Int -> SprintfType s
SprintfType (c:s) = SprintfType s
SprintfType [] = String

Now if you have a function

sprintf :: (s :: String) -> SprintfType s

it's really easy to use for static strings:

sprintf "hello" :: String
sprintf "%d %d" :: Int -> Int -> String

There are two problems to consider, however:

1) How do you write sprintf? You need to prove for each case that the type of function you are generating is equal to SprintfType s. This is not that hard; you just mirror the type level computation at the value level:

sprintf :: (s :: String) -> SprintfType s
sprintf = sprintf' id -- use CPS for the result

sprintf' :: (String -> String) -> (s :: String) -> SprintfType s
sprintf' k ('%':'d':rest) = \i -> sprintf' (\s -> k (show i ++ s)) rest
sprintf' k (c:rest) = sprintf' (\s -> k (c:s)) rest
sprintf' k [] = k []

I've noticed this as a common pattern in dependently typed programs; you write the same program twice, once at the type level and once at the value level. I wonder if there is a way to automate it?

2) What if you don't want to pass in a static string? Then you need to provide a proof that the type created by the string is the one you think it is. For example, you can write a theorem that for all strings s that do not contain the "%" character, SprintfType (x ++ s) = SprintfType x = SprintfType (s ++ x). Then you can apply that theorem when calling sprintf.

But that's a lot of work. It's a lot easier to just say "I know this is true", pass in something you believe is safe, and be done with it.

Then somebody figures out a way to get an unquoted "%s" through your security and writes a buffer overrun exploit because you didn't prove your safety property :)