A fully-fledged interpreter of a simple functional programming language, written in Haskell.
A well-typed interpreter is an interpreter in which an Abstract Syntax Tree is well-typed in Haskell only if it corresponds to a well-typed program in the interpreted language. It is a commonly used example that demonstrates the power of languages with dependent types, for example idris.
This is a research experiment to see how far can we go with the recently added limited dependent typing capabilities in Haskell. The main goal was to reproduce this paper in Haskell.
- Hindley–Milner type system
- Interacting with outside world using the IO monad
- Higher-order functions
- Lazy evaluation
- Row-polymorphic object system
- Integration with Haskell's module system
Everything you would expect from a language with global type inference. In most places you don't need to write types at all because they are inferred. This enables expressing algorithms in a clear and concise way. For example, quicksort can be written in just a few lines:
quicksort = let
mkQuicksort quicksort li =
if null li then [] else
let
lesser = tail li |> filter (< head li)
greater = tail li |> filter (>= head li)
in (quicksort lesser) ++ [head li] ++ (quicksort greater)
in fix mkQuicksort
Note the use of the fixpoint combinator fix mkQuicksort
to achieve recursion. To keep the core language simple and minimal, support for recursion is implemented through the fix
function in the standard library.
We can use the IO monad to read from stdin and write to stdout. We enclose sequences of IO operations using begin
and end
keywords, similarly to Haskell's do-notation:
open StdLib
main = begin
putStrLn "Hello World!"
putStrLn "What's your name?"
name : String <- getLine
putStrLn <| "Nice to meet you, " ++ name ++ "!"
end
Higher-order functions are fully supported, which means that you can use familiar programming patterns from other functional languages, such as using map and fold to iterate over collections, writing functions in continuation-passing style to implement sophisticated control flow, etc. Here is a small example:
open StdLib
mkMap map = fun f li ->
if null li then [] else f (head li) `cons` map f (tail li)
map = fix mkMap
mkConcat concat li =
if null li then [] else head li ++ (concat $ tail li)
concat = fix mkConcat
functions = [(+1), (+3), ( * 3)]
main = begin
putStrLn $ concat $ map (fun f -> show (f 2) ++ ", ") functions
(* This should print 3, 5, 6 *)
end
Lazy evaluation allows for manipulating potentially infinite data structures. Here is a program that creates infinite list of fibonacci numbers and later prints the first 10 of them:
open StdLib
fib = let
mkFib fib = zipWith (+) ([1] ++ fib) ([0, 1] ++ fib)
in fix mkFib
fib_prefix = take 10 fib
main = begin
putStrLn $ "First 10 numbers of Fibonacci sequence"
putStrLn $ show fib_prefix
end
Ability to construct objects that model entities and their relationships is an essential element of any programming language. WellTyped.hs achieves this goal by having a row-polymorphic object system, which allows expressing many data structures in a natural way.
open StdLib
encode token = "encoded " ++ token
secret = encode "secret_password"
HttpRequest url auth_token = object
url = url
headers = object
www_authenticate = "Basic realm=dummy"
authorization = encode auth_token
content_type = "application/json"
isAuthenticated request = request.headers.authorization == secret
main = begin
url : String <- getLine
token : String <- getLine
request = HttpRequest url token
if isAuthenticated request then
putStrLn "Authentication successful!"
else
putStrLn "Authentication failed!"
end
Programs written in WellTyped.hs can import modules written in Haskell. For example, standard library is implemented as a module that just exports relevant functions from Haskell's prelude: StdLib.hs
For example, a relevant section that exports input and output operations looks like this:
#include "extension_base.hs"
module StdLib where
import qualified Base
import Base (A, Type, eq_value, show_value)
io_ = [
EXPORT("bindIO", FORALL(a, b), (>>=) :: IO a -> (a -> IO b) -> IO b),
EXPORT("nextIO", FORALL(a, b), (>>) :: IO a -> IO b -> IO b),
EXPORT("returnIO", FORALL(a), return :: a -> IO a),
EXPORT("return", FORALL(a), return :: a -> IO a),
EXPORT("failIO", FORALL(a), fail :: String -> IO a),
EXPORT("mapM_", FORALL(a, b), mapM_ :: (a -> IO b) -> [a] -> IO ()),
EXPORT("mapM", FORALL(a, b), mapM :: (a -> IO b) -> [a] -> IO [b]),
EXPORT("sequence", FORALL(a), sequence_ :: [IO a] -> IO ()),
EXPORT("sequence_", FORALL(a), sequence :: [IO a] -> IO [a]),
EXPORT("putChar", NONE, putChar :: Char -> IO ()),
EXPORT("putStr", NONE, putStr :: String -> IO ()),
EXPORT("putStrLn", NONE, putStrLn :: String -> IO ()),
EXPORT("print", FORALL(a), (putStrLn . show_value) :: A Type a => a -> IO ()),
EXPORT("getChar", NONE, getChar :: IO Char),
EXPORT("getLine", NONE, getLine :: IO String),
EXPORT("getContents", NONE, getContents :: IO String),
EXPORT("interact", NONE, interact :: (String -> String) -> IO ()),
EXPORT("readFile", NONE, readFile :: FilePath -> IO String),
EXPORT("writeFile", NONE, writeFile :: FilePath -> String -> IO ()),
EXPORT("appendFile", NONE, appendFile :: FilePath -> String -> IO ())
]