diff --git a/libraries/prelude/prelude.purs b/libraries/prelude/prelude.purs
--- a/libraries/prelude/prelude.purs
+++ b/libraries/prelude/prelude.purs
@@ -1,5 +1,11 @@
 module Prelude where
 
+  foreign import data String :: *
+  foreign import data Number :: *
+  foreign import data Boolean :: *
+  foreign import data Array :: * -> *
+  foreign import data Function :: * -> * -> *
+
   id :: forall a. a -> a
   id = \x -> x
 
@@ -401,28 +407,76 @@
 
 module Math where
 
-  type Math = 
-    { abs :: Number -> Number
-    , acos :: Number -> Number
-    , asin :: Number -> Number
-    , atan :: Number -> Number
-    , atan2 :: (Number, Number) -> Number
-    , aceil :: Number -> Number
-    , cos :: Number -> Number
-    , exp :: Number -> Number
-    , floor :: Number -> Number
-    , log :: Number -> Number
-    , max :: (Number, Number) -> Number
-    , pow :: (Number, Number) -> Number
-    , random :: () -> Number
-    , round :: Number -> Number
-    , sin :: Number -> Number
-    , sqrt :: Number -> Number
-    , tan :: Number -> Number
-    }
+  foreign import abs "function abs(n){\
+                     \  return Math.abs(n);\
+                     \}" :: Number -> Number
 
-  foreign import math "var math = Math;" :: Math
-  
+  foreign import acos "function acos(n){\
+                      \  return Math.acos(n);\
+                      \}" :: Number -> Number
+
+  foreign import asin "function asin(n){\
+                      \  return Math.asin(n);\
+                      \}" :: Number -> Number
+
+  foreign import atan "function atan(n){\
+                      \  return Math.atan(n);\
+                      \}" :: Number -> Number
+
+  foreign import atan2 "function atan2(y){\
+                       \  return function (x) {\
+                       \    return Math.atan2(y, x);\
+                       \  };\
+                       \}" :: Number -> Number -> Number
+
+  foreign import aceil "function aceil(n){\
+                       \  return Math.aceil(n);\
+                       \}" :: Number -> Number
+
+  foreign import cos "function cos(n){\
+                     \  return Math.cos(n);\
+                     \}" :: Number -> Number
+
+  foreign import exp "function exp(n){\
+                     \  return Math.exp(n);\
+                     \}" :: Number -> Number
+
+  foreign import floor "function floor(n){\
+                       \  return Math.floor(n);\
+                       \}" :: Number -> Number
+
+  foreign import log "function log(n){\
+                     \  return Math.log(n);\
+                     \}" :: Number -> Number
+
+  foreign import max "function max(n){\
+                     \  return Math.max(n);\
+                     \}" :: Number -> Number
+
+  foreign import min "function min(n){\
+                     \  return Math.min(n);\
+                     \}" :: Number -> Number
+
+  foreign import pow "function pow(n){\
+                     \  return Math.pow(n);\
+                     \}" :: Number -> Number
+
+  foreign import round "function round(n){\
+                       \  return Math.round(n);\
+                       \}" :: Number -> Number
+
+  foreign import sin "function sin(n){\
+                     \  return Math.sin(n);\
+                     \}" :: Number -> Number
+
+  foreign import sqrt "function sqrt(n){\
+                      \  return Math.sqrt(n);\
+                      \}" :: Number -> Number
+
+  foreign import tan "function tan(n){\
+                     \  return Math.tan(n);\
+                     \}" :: Number -> Number
+
 module Eff where
 
   foreign import data Eff :: # ! -> * -> *
@@ -450,6 +504,18 @@
   instance Prelude.Monad (Eff e) where
     ret = retEff
     (>>=) = bindEff
+
+module Random where
+
+  import Eff
+
+  foreign import data Random :: !
+
+  foreign import random "function random() {\
+                        \  return function() {\
+                        \    return Math.random();\
+                        \  };\
+                        \}" :: forall e. Eff (random :: Random | e) Number
 
 module Errors where
 
diff --git a/psci/Main.hs b/psci/Main.hs
--- a/psci/Main.hs
+++ b/psci/Main.hs
@@ -64,7 +64,7 @@
     trace = P.Var (P.Qualified (Just traceModule) (P.Ident "print"))
     mainDecl = P.ValueDeclaration (P.Ident "main") [] Nothing
         (P.Do [ P.DoNotationBind (P.VarBinder (P.Ident "it")) value
-              , P.DoNotationValue (P.App trace [ P.Var (P.Qualified Nothing (P.Ident "it")) ] )
+              , P.DoNotationValue (P.App trace (P.Var (P.Qualified Nothing (P.Ident "it"))) )
               ])
   in
     P.Module moduleName $ map (importDecl . P.ModuleName) imports ++ [mainDecl]
diff --git a/purescript.cabal b/purescript.cabal
--- a/purescript.cabal
+++ b/purescript.cabal
@@ -1,5 +1,5 @@
 name: purescript
-version: 0.3.6.1
+version: 0.3.7
 cabal-version: >=1.8
 build-type: Simple
 license: MIT
diff --git a/src/Language/PureScript/CodeGen/JS.hs b/src/Language/PureScript/CodeGen/JS.hs
--- a/src/Language/PureScript/CodeGen/JS.hs
+++ b/src/Language/PureScript/CodeGen/JS.hs
@@ -110,9 +110,9 @@
 valueToJs opts m e (IfThenElse cond th el) = JSConditional (valueToJs opts m e cond) (valueToJs opts m e th) (valueToJs opts m e el)
 valueToJs opts m e (Accessor prop val) = JSAccessor prop (valueToJs opts m e val)
 valueToJs opts m e (Indexer index val) = JSIndexer (valueToJs opts m e index) (valueToJs opts m e val)
-valueToJs opts m e (App val args) = JSApp (valueToJs opts m e val) (map (valueToJs opts m e) args)
-valueToJs opts m e (Abs args val) = JSFunction Nothing args (JSBlock [JSReturn (valueToJs opts m e val)])
-valueToJs opts m e (TypedValue _ (Abs args val) ty) | optionsPerformRuntimeTypeChecks opts = JSFunction Nothing args (JSBlock $ runtimeTypeChecks args ty ++ [JSReturn (valueToJs opts m e val)])
+valueToJs opts m e (App val arg) = JSApp (valueToJs opts m e val) [valueToJs opts m e arg]
+valueToJs opts m e (Abs arg val) = JSFunction Nothing [arg] (JSBlock [JSReturn (valueToJs opts m e val)])
+valueToJs opts m e (TypedValue _ (Abs arg val) ty) | optionsPerformRuntimeTypeChecks opts = JSFunction Nothing [arg] (JSBlock $ runtimeTypeChecks arg ty ++ [JSReturn (valueToJs opts m e val)])
 valueToJs opts m e (Unary op val) = JSUnary op (valueToJs opts m e val)
 valueToJs opts m e (Binary op v1 v2) = JSBinary op (valueToJs opts m e v1) (valueToJs opts m e v2)
 valueToJs _ m e (Var ident) = varToJs m e ident
@@ -120,28 +120,28 @@
 valueToJs _ _ _ (TypeClassDictionary _ _) = error "Type class dictionary was not replaced"
 valueToJs _ _ _ _ = error "Invalid argument to valueToJs"
 
-runtimeTypeChecks :: [Ident] -> Type -> [JS]
-runtimeTypeChecks args ty =
+runtimeTypeChecks :: Ident -> Type -> [JS]
+runtimeTypeChecks arg ty =
   let
-    argTys = getFunctionArgumentTypes ty
+    argTy = getFunctionArgumentType ty
   in
-    concat $ zipWith argumentCheck (map JSVar args) argTys
+    maybe [] (argumentCheck (JSVar arg)) argTy
   where
-  getFunctionArgumentTypes :: Type -> [Type]
-  getFunctionArgumentTypes (Function funArgs _) = funArgs
-  getFunctionArgumentTypes (ForAll _ ty') = getFunctionArgumentTypes ty'
-  getFunctionArgumentTypes _ = []
+  getFunctionArgumentType :: Type -> Maybe Type
+  getFunctionArgumentType (TypeApp (TypeApp t funArg) _) | t == tyFunction = Just funArg
+  getFunctionArgumentType (ForAll _ ty') = getFunctionArgumentType ty'
+  getFunctionArgumentType _ = Nothing
   argumentCheck :: JS -> Type -> [JS]
-  argumentCheck val Number = [typeCheck val "number"]
-  argumentCheck val String = [typeCheck val "string"]
-  argumentCheck val Boolean = [typeCheck val "boolean"]
-  argumentCheck val (TypeApp Array _) = [arrayCheck val]
+  argumentCheck val t | t == tyNumber = [typeCheck val "number"]
+  argumentCheck val t | t == tyString = [typeCheck val "string"]
+  argumentCheck val t | t == tyBoolean = [typeCheck val "boolean"]
+  argumentCheck val (TypeApp t _) | t == tyArray = [arrayCheck val]
   argumentCheck val (Object row) =
     let
       (pairs, _) = rowToList row
     in
       typeCheck val "object" : concatMap (\(prop, ty') -> argumentCheck (JSAccessor prop val) ty') pairs
-  argumentCheck val (Function _ _) = [typeCheck val "function"]
+  argumentCheck val (TypeApp (TypeApp t _) _) | t == tyFunction = [typeCheck val "function"]
   argumentCheck val (ForAll _ ty') = argumentCheck val ty'
   argumentCheck _ _ = []
   typeCheck :: JS -> String -> JS
@@ -253,7 +253,7 @@
   numConstructors ty = length $ filter (\(ty1, _) -> ((==) `on` typeConstructor) ty ty1) $ M.elems $ dataConstructors e
   typeConstructor (TypeConstructor qual) = qualify m qual
   typeConstructor (ForAll _ ty) = typeConstructor ty
-  typeConstructor (Function _ ty) = typeConstructor ty
+  typeConstructor (TypeApp (TypeApp t _) ty) | t == tyFunction = typeConstructor ty
   typeConstructor (TypeApp ty _) = typeConstructor ty
   typeConstructor fn = error $ "Invalid arguments to typeConstructor: " ++ show fn
 
diff --git a/src/Language/PureScript/Declarations.hs b/src/Language/PureScript/Declarations.hs
--- a/src/Language/PureScript/Declarations.hs
+++ b/src/Language/PureScript/Declarations.hs
@@ -88,7 +88,7 @@
   -- |
   -- A value declaration (name, top-level binders, optional guard, value)
   --
-  | ValueDeclaration Ident [[Binder]] (Maybe Guard) Value
+  | ValueDeclaration Ident [Binder] (Maybe Guard) Value
   -- |
   -- A minimal mutually recursive set of value declarations
   --
diff --git a/src/Language/PureScript/Names.hs b/src/Language/PureScript/Names.hs
--- a/src/Language/PureScript/Names.hs
+++ b/src/Language/PureScript/Names.hs
@@ -30,11 +30,16 @@
   -- |
   -- A symbolic name for an infix operator
   --
-  | Op String deriving (Eq, Ord, Data, Typeable)
+  | Op String
+  -- |
+  -- An escaped name
+  --
+  | Escaped String deriving (Eq, Ord, Data, Typeable)
 
 instance Show Ident where
   show (Ident s) = s
   show (Op op) = '(':op ++ ")"
+  show (Escaped s) = s
 
 -- |
 -- Proper names, i.e. capitalized names for e.g. module names, type//data constructors.
diff --git a/src/Language/PureScript/Parser/Declarations.hs b/src/Language/PureScript/Parser/Declarations.hs
--- a/src/Language/PureScript/Parser/Declarations.hs
+++ b/src/Language/PureScript/Parser/Declarations.hs
@@ -58,12 +58,9 @@
 parseValueDeclaration :: P.Parsec String ParseState Declaration
 parseValueDeclaration =
   ValueDeclaration <$> parseNonReservedIdent
-                   <*> P.many parseTopLevelBinder
+                   <*> P.many parseBinderNoParens
                    <*> P.optionMaybe parseGuard
                    <*> ((lexeme (indented *> P.char '=')) *> parseValue)
-
-parseTopLevelBinder :: P.Parsec String ParseState [Binder]
-parseTopLevelBinder = return <$> P.try parseBinderNoParens <|> parens (commaSep parseBinder)
 
 parseExternDeclaration :: P.Parsec String ParseState Declaration
 parseExternDeclaration = P.try (reserved "foreign") *> indented *> (reserved "import") *> indented *>
diff --git a/src/Language/PureScript/Parser/Types.hs b/src/Language/PureScript/Parser/Types.hs
--- a/src/Language/PureScript/Parser/Types.hs
+++ b/src/Language/PureScript/Parser/Types.hs
@@ -27,30 +27,26 @@
 import Control.Monad (when, unless)
 
 parseNumber :: P.Parsec String ParseState Type
-parseNumber = const Number <$> reserved "Number"
+parseNumber = const tyNumber <$> reserved "Number"
 
 parseString :: P.Parsec String ParseState Type
-parseString = const String <$> reserved "String"
+parseString = const tyString <$> reserved "String"
 
 parseBoolean :: P.Parsec String ParseState Type
-parseBoolean = const Boolean <$> reserved "Boolean"
+parseBoolean = const tyBoolean <$> reserved "Boolean"
 
 parseArray :: P.Parsec String ParseState Type
-parseArray = squares $ return Array
+parseArray = squares $ return tyArray
 
 parseArrayOf :: P.Parsec String ParseState Type
-parseArrayOf = squares $ TypeApp Array <$> parseType
+parseArrayOf = squares $ TypeApp tyArray <$> parseType
 
+parseFunction :: P.Parsec String ParseState Type
+parseFunction = parens $ P.try (lexeme (P.string "->")) >> return tyFunction
+
 parseObject :: P.Parsec String ParseState Type
 parseObject = braces $ Object <$> parseRow False
 
-parseFunction :: P.Parsec String ParseState Type
-parseFunction = do
-  args <- lexeme $ parens $ commaSep parsePolyType
-  _ <- lexeme $ P.string "->"
-  resultType <- parseType
-  return $ Function args resultType
-
 parseTypeVariable :: P.Parsec String ParseState Type
 parseTypeVariable = TypeVar <$> identifier
 
@@ -68,12 +64,13 @@
             , parseBoolean
             , parseArray
             , parseArrayOf
+            , parseFunction
             , parseObject
             , parseTypeVariable
             , parseTypeConstructor
             , parseForAll
             , parens (parseRow True)
-            , parens parseType ])
+            , parens parsePolyType ])
 
 parseConstrainedType :: P.Parsec String ParseState Type
 parseConstrainedType = do
@@ -90,10 +87,10 @@
   return $ maybe ty (flip ConstrainedType ty) constraints
 
 parseAnyType :: P.Parsec String ParseState Type
-parseAnyType = (P.buildExpressionParser operators $ parseTypeAtom) <|> parseFunction P.<?> "type"
+parseAnyType = (P.buildExpressionParser operators $ parseTypeAtom) P.<?> "type"
   where
   operators = [ [ P.Infix (return TypeApp) P.AssocLeft ]
-              , [ P.Infix (P.try (lexeme (P.string "->")) >> return (\t1 t2 -> Function [t1] t2)) P.AssocRight ] ]
+              , [ P.Infix (P.try (lexeme (P.string "->")) >> return function) P.AssocRight ] ]
 
 -- |
 -- Parse a monotype
@@ -110,7 +107,6 @@
 parsePolyType :: P.Parsec String ParseState Type
 parsePolyType = do
   ty <- parseAnyType
-  unless (isPolyType ty) $ P.unexpected "polymorphic type"
   return ty
 
 parseNameAndType :: P.Parsec String ParseState t -> P.Parsec String ParseState (String, t)
diff --git a/src/Language/PureScript/Parser/Values.hs b/src/Language/PureScript/Parser/Values.hs
--- a/src/Language/PureScript/Parser/Values.hs
+++ b/src/Language/PureScript/Parser/Values.hs
@@ -54,19 +54,12 @@
 parseAbs :: P.Parsec String ParseState Value
 parseAbs = do
   C.reservedOp "\\"
-  args <- P.many (C.indented *> (P.try singleArg <|> manyArgs))
+  args <- P.many1 (C.indented *> (Abs <$> C.parseIdent))
   C.indented *> C.reservedOp "->"
   value <- parseValue
   return $ toFunction args value
   where
-  manyArgs :: P.Parsec String ParseState (Value -> Value)
-  manyArgs = do
-    args <- C.parens (C.commaSep C.parseIdent)
-    return $ Abs args
-  singleArg :: P.Parsec String ParseState (Value -> Value)
-  singleArg = Abs . return <$> C.parseIdent
   toFunction :: [Value -> Value] -> Value -> Value
-  toFunction [] value = Abs [] value
   toFunction args value = foldr (($)) value args
 
 parseVar :: P.Parsec String ParseState Value
@@ -159,8 +152,7 @@
   indexersAndAccessors = C.buildPostfixParser postfixTable1 parseValueAtom
   postfixTable1 = [ parseAccessor
                   , \v -> P.try $ flip ObjectUpdate <$> (C.indented *> C.braces (C.commaSep1 (C.indented *> parsePropertyUpdate))) <*> pure v ]
-  postfixTable2 = [ \v -> P.try (C.indented *> indexersAndAccessors >>= \t2 -> return (\t1 -> App t1 [t2])) <*> pure v
-                  , \v -> P.try $ flip App <$> (C.indented *> C.parens (C.commaSep parseValue)) <*> pure v
+  postfixTable2 = [ \v -> P.try (C.indented *> indexersAndAccessors >>= return . flip App) <*> pure v
                   , \v -> flip (TypedValue True) <$> (P.try (C.lexeme (C.indented *> P.string "::")) *> parsePolyType) <*> pure v
                   ]
   operators = [ [ Prefix $ C.lexeme (P.try $ C.indented *> C.reservedOp "!") >> return (Unary Not)
diff --git a/src/Language/PureScript/Pretty/Common.hs b/src/Language/PureScript/Pretty/Common.hs
--- a/src/Language/PureScript/Pretty/Common.hs
+++ b/src/Language/PureScript/Pretty/Common.hs
@@ -36,10 +36,31 @@
 identToJs :: Ident -> String
 identToJs (Ident name) = concatMap identCharToString name
 identToJs (Op op) = concatMap identCharToString op
+identToJs (Escaped name) = name
 
 identCharToString :: Char -> String
 identCharToString c | isAlphaNum c = [c]
 identCharToString '_' = "_"
+identCharToString '.' = "$dot"
+identCharToString '$' = "$dollar"
+identCharToString '~' = "$tilde"
+identCharToString '=' = "$eq"
+identCharToString '<' = "$less"
+identCharToString '>' = "$greater"
+identCharToString '!' = "$bang"
+identCharToString '#' = "$hash"
+identCharToString '%' = "$percent"
+identCharToString '^' = "$up"
+identCharToString '&' = "$amp"
+identCharToString '|' = "$bar"
+identCharToString '*' = "$times"
+identCharToString '/' = "$div"
+identCharToString '+' = "$plus"
+identCharToString '-' = "$minus"
+identCharToString ':' = "$colon"
+identCharToString '\\' = "$bslash"
+identCharToString '?' = "$qmark"
+identCharToString '@' = "$at"
 identCharToString c = '$' : show (ord c)
 
 -- |
diff --git a/src/Language/PureScript/Pretty/Types.hs b/src/Language/PureScript/Pretty/Types.hs
--- a/src/Language/PureScript/Pretty/Types.hs
+++ b/src/Language/PureScript/Pretty/Types.hs
@@ -31,12 +31,9 @@
 typeLiterals :: Pattern () Type String
 typeLiterals = mkPattern match
   where
-  match Number = Just "Number"
-  match String = Just "String"
-  match Boolean = Just "Boolean"
-  match Array = Just $ "[]"
   match (Object row) = Just $ "{ " ++ prettyPrintType row ++ " }"
   match (TypeVar var) = Just var
+  match (TypeApp arr ty) | arr == tyArray = Just $ "[" ++ prettyPrintType ty ++ "]"
   match (TypeConstructor ctor) = Just $ show ctor
   match (TUnknown (TypedUnknown (Unknown u))) = Just $ 'u' : show u
   match (Skolem s) = Just $ 's' : show s
@@ -74,13 +71,7 @@
 singleArgumentFunction :: Pattern () Type (Type, Type)
 singleArgumentFunction = mkPattern match
   where
-  match (Function [arg] ret) = Just (arg, ret)
-  match _ = Nothing
-
-function :: Pattern () Type ([Type], Type)
-function = mkPattern match
-  where
-  match (Function args ret) = Just (args, ret)
+  match (TypeApp (TypeApp t arg) ret) | t == tyFunction = Just (arg, ret)
   match _ = Nothing
 
 -- |
@@ -95,6 +86,5 @@
   operators =
     OperatorTable [ [ AssocL typeApp $ \f x -> f ++ " " ++ x ]
                   , [ AssocR singleArgumentFunction $ \arg ret -> arg ++ " -> " ++ ret
-                    , Wrap function $ \args ret -> "(" ++ intercalate ", " (map prettyPrintType args) ++ ") -> " ++ ret
                     ]
                   ]
diff --git a/src/Language/PureScript/Pretty/Values.hs b/src/Language/PureScript/Pretty/Values.hs
--- a/src/Language/PureScript/Pretty/Values.hs
+++ b/src/Language/PureScript/Pretty/Values.hs
@@ -77,13 +77,13 @@
 app :: Pattern () Value (String, Value)
 app = mkPattern match
   where
-  match (App val args) = Just (intercalate "," (map prettyPrintValue args), val)
+  match (App val arg) = Just (prettyPrintValue arg, val)
   match _ = Nothing
 
-lam :: Pattern () Value ([String], Value)
+lam :: Pattern () Value (String, Value)
 lam = mkPattern match
   where
-  match (Abs args val) = Just (map show args, val)
+  match (Abs arg val) = Just (show arg, val)
   match _ = Nothing
 
 typed :: Pattern () Value (Type, Value)
@@ -127,8 +127,8 @@
   operators =
     OperatorTable [ [ Wrap accessor $ \prop val -> val ++ "." ++ prop ]
                   , [ Wrap objectUpdate $ \ps val -> val ++ "{ " ++ intercalate ", " ps ++ " }" ]
-                  , [ Wrap app $ \args val -> val ++ "(" ++ args ++ ")" ]
-                  , [ Split lam $ \args val -> "\\" ++ intercalate ", " args ++ " -> " ++ prettyPrintValue val ]
+                  , [ Wrap app $ \arg val -> val ++ "(" ++ arg ++ ")" ]
+                  , [ Split lam $ \arg val -> "\\" ++ arg ++ " -> " ++ prettyPrintValue val ]
                   , [ Wrap ifThenElse $ \(th, el) cond -> cond ++ " ? " ++ prettyPrintValue th ++ " : " ++ prettyPrintValue el ]
                   , [ Wrap typed $ \ty val -> val ++ " :: " ++ prettyPrintType ty ]
                   , [ AssocR indexer (\index val -> val ++ " !! " ++ index) ]
diff --git a/src/Language/PureScript/Scope.hs b/src/Language/PureScript/Scope.hs
--- a/src/Language/PureScript/Scope.hs
+++ b/src/Language/PureScript/Scope.hs
@@ -33,7 +33,7 @@
 usedNames val = nub $ everything (++) (mkQ [] namesV `extQ` namesS `extQ` namesB `extQ` namesJS) val
   where
   namesV :: Value -> [Ident]
-  namesV (Abs args _) = args
+  namesV (Abs arg _) = [arg]
   namesV (Var (Qualified Nothing name)) = [name]
   namesV _ = []
   namesS :: Statement -> [Ident]
diff --git a/src/Language/PureScript/Sugar/CaseDeclarations.hs b/src/Language/PureScript/Sugar/CaseDeclarations.hs
--- a/src/Language/PureScript/Sugar/CaseDeclarations.hs
+++ b/src/Language/PureScript/Sugar/CaseDeclarations.hs
@@ -48,27 +48,23 @@
 toDecls d@[ValueDeclaration _ [] Nothing _] = return d
 toDecls ds@(ValueDeclaration ident bs _ _ : _) = do
   let tuples = map toTuple ds
-  unless (all ((== map length bs) . map length . fst) tuples) $
+  unless (all ((== length bs) . length . fst) tuples) $
       throwError $ "Argument list lengths differ in declaration " ++ show ident
   return [makeCaseDeclaration ident tuples]
 toDecls ds = return ds
 
-toTuple :: Declaration -> ([[Binder]], (Maybe Guard, Value))
+toTuple :: Declaration -> ([Binder], (Maybe Guard, Value))
 toTuple (ValueDeclaration _ bs g val) = (bs, (g, val))
 toTuple _ = error "Not a value declaration"
 
-makeCaseDeclaration :: Ident -> [([[Binder]], (Maybe Guard, Value))] -> Declaration
+makeCaseDeclaration :: Ident -> [([Binder], (Maybe Guard, Value))] -> Declaration
 makeCaseDeclaration ident alternatives =
   let
-    argPattern = map length . fst . head $ alternatives
-    args = take (sum argPattern) $ unusedNames (ident, alternatives)
+    argPattern = length . fst . head $ alternatives
+    args = take argPattern $ unusedNames (ident, alternatives)
     vars = map (\arg -> Var (Qualified Nothing arg)) args
-    binders = [ (join bs, g, val) | (bs, (g, val)) <- alternatives ]
-    value = foldr (\args' ret -> Abs args' ret) (Case vars binders) (rearrange argPattern args)
+    binders = [ (bs, g, val) | (bs, (g, val)) <- alternatives ]
+    value = foldr (\args' ret -> Abs args' ret) (Case vars binders) args
   in
     ValueDeclaration ident [] Nothing value
-
-rearrange :: [Int] -> [a] -> [[a]]
-rearrange [] _ = []
-rearrange (n:ns) xs = take n xs : rearrange ns (drop n xs)
 
diff --git a/src/Language/PureScript/Sugar/DoNotation.hs b/src/Language/PureScript/Sugar/DoNotation.hs
--- a/src/Language/PureScript/Sugar/DoNotation.hs
+++ b/src/Language/PureScript/Sugar/DoNotation.hs
@@ -46,16 +46,16 @@
   go [DoNotationValue val] = return val
   go (DoNotationValue val : rest) = do
     rest' <- go rest
-    return $ App (App bind [val]) [Abs [Ident "_"] rest']
+    return $ App (App bind val) (Abs (Ident "_") rest')
   go [DoNotationBind _ _] = Left "Bind statement cannot be the last statement in a do block"
   go (DoNotationBind NullBinder val : rest) = go (DoNotationValue val : rest)
   go (DoNotationBind (VarBinder ident) val : rest) = do
     rest' <- go rest
-    return $ App (App bind [val]) [Abs [ident] rest']
+    return $ App (App bind val) (Abs ident rest')
   go (DoNotationBind binder val : rest) = do
     rest' <- go rest
     let ident = head $ unusedNames rest'
-    return $ App (App bind [val]) [Abs [ident] (Case [Var (Qualified Nothing ident)] [([binder], Nothing, rest')])]
+    return $ App (App bind val) (Abs ident (Case [Var (Qualified Nothing ident)] [([binder], Nothing, rest')]))
   go [DoNotationLet _ _] = Left "Let statement cannot be the last statement in a do block"
   go (DoNotationLet binder val : rest) = do
     rest' <- go rest
diff --git a/src/Language/PureScript/Sugar/Operators.hs b/src/Language/PureScript/Sugar/Operators.hs
--- a/src/Language/PureScript/Sugar/Operators.hs
+++ b/src/Language/PureScript/Sugar/Operators.hs
@@ -58,7 +58,7 @@
 customOperatorTable :: M.Map (Qualified Ident) Fixity -> [[(Qualified Ident, Value -> Value -> Value, Associativity)]]
 customOperatorTable fixities =
   let
-    applyUserOp name t1 t2 = App (App (Var name) [t1]) [t2]
+    applyUserOp name t1 t2 = App (App (Var name) t1) t2
     userOps = map (\(name, Fixity a p) -> (name, applyUserOp name, p, a)) . M.toList $ fixities
     sorted = sortBy (compare `on` (\(_, _, p, _) -> p)) (userOps ++ builtIns)
     groups = groupBy ((==) `on` (\(_, _, p, _) -> p)) sorted
@@ -79,7 +79,7 @@
   bracketChain :: Chain -> Either String Value
   bracketChain = either (Left . show) Right . P.parse (P.buildExpressionParser opTable parseValue <* P.eof) "operator expression"
   opTable = map (map (\(name, f, a) -> P.Infix (P.try (matchOp moduleName name) >> return f) (toAssoc a))) ops
-    ++ [[P.Infix (P.try (parseOp >>= \ident -> return (\t1 t2 -> App (App (Var ident) [t1]) [t2]))) P.AssocLeft]]
+    ++ [[P.Infix (P.try (parseOp >>= \ident -> return (\t1 t2 -> App (App (Var ident) t1) t2))) P.AssocLeft]]
 
 toAssoc :: Associativity -> P.Assoc
 toAssoc Infixl = P.AssocLeft
diff --git a/src/Language/PureScript/Sugar/TypeClasses.hs b/src/Language/PureScript/Sugar/TypeClasses.hs
--- a/src/Language/PureScript/Sugar/TypeClasses.hs
+++ b/src/Language/PureScript/Sugar/TypeClasses.hs
@@ -87,10 +87,8 @@
   memberNames <- mapM (memberToNameAndValue memberTypes) decls
   return $ ValueDeclaration entryName [] Nothing
     (TypedValue True
-      (Abs
-        (map (\n -> Ident ('_' : show n)) [1..length deps])
-        (ObjectLiteral memberNames))
-      (quantify (Function (map (\(pn, ty') -> TypeApp (TypeConstructor pn) ty') deps) (TypeApp (TypeConstructor name) ty)))
+      (foldr Abs (ObjectLiteral memberNames) (map (\n -> Ident ('_' : show n)) [1..length deps]))
+      (quantify (foldr function (TypeApp (TypeConstructor name) ty) (map (\(pn, ty') -> TypeApp (TypeConstructor pn) ty') deps)))
     )
   where
   memberToNameAndValue :: [(String, Type)] -> Declaration -> Desugar (String, Value)
@@ -99,20 +97,22 @@
     memberName <- mkDictionaryEntryName mn name ty ident
     return (identToJs ident, TypedValue False
                                (if null deps then Var (Qualified Nothing memberName)
-                                else App (Var (Qualified Nothing memberName)) (map (\n -> Var (Qualified Nothing (Ident ('_' : show n)))) [1..length deps]))
+                                else foldl App (Var (Qualified Nothing memberName)) (map (\n -> Var (Qualified Nothing (Ident ('_' : show n)))) [1..length deps]))
                                (quantify memberType))
   memberToNameAndValue _ _ = error "Invalid declaration in type instance definition"
 
 typeInstanceDictionaryEntryDeclaration :: ModuleName -> [(Qualified ProperName, Type)] -> Qualified ProperName -> Type -> Declaration -> Desugar Declaration
 typeInstanceDictionaryEntryDeclaration mn deps name ty (ValueDeclaration ident [] _ val) = do
   m <- get
-  valTy <- lift $ maybe (Left $ "Type class " ++ show name ++ " is undefined. Type class names must be qualified.") Right $
-                do (arg, members) <- M.lookup (qualify mn name) m
-                   ty' <- lookup (identToJs ident) members
-                   return $ replaceTypeVars arg ty ty'
+  valTy <- lift $ do (arg, members) <- lookupTypeClass m
+                     ty' <- lookupIdent members
+                     return $ replaceTypeVars arg ty ty'
   entryName <- mkDictionaryEntryName mn name ty ident
   return $ ValueDeclaration entryName [] Nothing
     (TypedValue True val (quantify (if null deps then valTy else ConstrainedType deps valTy)))
+  where
+  lookupTypeClass m = maybe (Left $ "Type class " ++ show name ++ " is undefined. Type class names must be qualified.") Right $ M.lookup (qualify mn name) m
+  lookupIdent members = maybe (Left $ "Type class " ++ show name ++ " does not have method " ++ show ident) Right $ lookup (identToJs ident) members
 typeInstanceDictionaryEntryDeclaration _ _ _ _ _ = error "Invalid declaration in type instance definition"
 
 qualifiedToString :: ModuleName -> Qualified ProperName -> String
@@ -135,14 +135,10 @@
   return $ Ident $ "__" ++ qualifiedToString mn cl ++ "_" ++ tyStr
 
 typeToString :: ModuleName -> Type -> Either String String
-typeToString _ String = return "string"
-typeToString _ Number = return "number"
-typeToString _ Boolean = return "boolean"
-typeToString _ Array = return "array"
 typeToString _ (TypeVar _) = return "var"
 typeToString mn (TypeConstructor ty') = return $ qualifiedToString mn ty'
 typeToString mn (TypeApp ty' (TypeVar _)) = typeToString mn ty'
-typeToString a b = Left $ "Type class instance must be of the form T a1 ... an " ++ show (a, b)
+typeToString _ _ = Left "Type class instance must be of the form T a1 ... an"
 
 -- |
 -- Generate a name for a type class dictionary member, based on the module name, class name, type name and
@@ -151,4 +147,4 @@
 mkDictionaryEntryName :: ModuleName -> Qualified ProperName -> Type -> Ident -> Desugar Ident
 mkDictionaryEntryName mn name ty ident = do
   Ident dictName <- lift $ mkDictionaryValueName mn name ty
-  return $ Ident $ dictName ++ "_" ++ identToJs ident
+  return $ Escaped $ dictName ++ "_" ++ identToJs ident
diff --git a/src/Language/PureScript/TypeChecker.hs b/src/Language/PureScript/TypeChecker.hs
--- a/src/Language/PureScript/TypeChecker.hs
+++ b/src/Language/PureScript/TypeChecker.hs
@@ -51,7 +51,7 @@
   env <- getEnv
   dataConstructorIsNotDefined moduleName dctor
   let retTy = foldl TypeApp (TypeConstructor (Qualified (Just moduleName) name)) (map TypeVar args)
-  let dctorTy = maybe retTy (\ty -> Function [ty] retTy) maybeTy
+  let dctorTy = maybe retTy (flip function retTy) maybeTy
   let polyType = mkForAll args dctorTy
   putEnv $ env { dataConstructors = M.insert (moduleName, dctor) (qualifyAllUnqualifiedNames moduleName env polyType, DataConstructor) (dataConstructors env) }
 
@@ -231,7 +231,7 @@
   constructs (TypeConstructor (Qualified (Just mn) pn')) pn
     = mn == moduleName && pn' == pn
   constructs (ForAll _ ty) pn = ty `constructs` pn
-  constructs (Function _ ty) pn = ty `constructs` pn
+  constructs (TypeApp (TypeApp t _) ty) pn | t == tyFunction = ty `constructs` pn
   constructs (TypeApp ty _) pn = ty `constructs` pn
   constructs fn _ = error $ "Invalid arguments to constructs: " ++ show fn
 typeCheckAll moduleName (d@(TypeClassDeclaration _ _ _) : rest) = do
diff --git a/src/Language/PureScript/TypeChecker/Kinds.hs b/src/Language/PureScript/TypeChecker/Kinds.hs
--- a/src/Language/PureScript/TypeChecker/Kinds.hs
+++ b/src/Language/PureScript/TypeChecker/Kinds.hs
@@ -117,19 +117,9 @@
 -- Infer a kind for a type
 --
 infer :: Type -> UnifyT Check Kind
-infer Number = return Star
-infer String = return Star
-infer Boolean = return Star
-infer Array = return $ FunKind Star Star
 infer (Object row) = do
   k <- infer row
   k ?= Row Star
-  return Star
-infer (Function args ret) = do
-  ks <- mapM infer args
-  k <- infer ret
-  k ?= Star
-  forM_ ks (?= Star)
   return Star
 infer (TypeVar v) = do
   Just moduleName <- checkCurrentModule <$> get
diff --git a/src/Language/PureScript/TypeChecker/Types.hs b/src/Language/PureScript/TypeChecker/Types.hs
--- a/src/Language/PureScript/TypeChecker/Types.hs
+++ b/src/Language/PureScript/TypeChecker/Types.hs
@@ -95,15 +95,7 @@
     sk <- skolemize ident ty1
     sk `unifyTypes` ty2
   unifyTypes' ty f@(ForAll _ _) = f `unifyTypes` ty
-  unifyTypes' Number Number = return ()
-  unifyTypes' String String = return ()
-  unifyTypes' Boolean Boolean = return ()
-  unifyTypes' Array Array = return ()
   unifyTypes' (Object row1) (Object row2) = row1 ?= row2
-  unifyTypes' (Function args1 ret1) (Function args2 ret2) = do
-    guardWith "Function applied to incorrect number of args" $ length args1 == length args2
-    zipWithM_ unifyTypes args1 args2
-    ret1 `unifyTypes` ret2
   unifyTypes' (TypeVar v1) (TypeVar v2) | v1 == v2 = return ()
   unifyTypes' (TypeConstructor c1) (TypeConstructor c2) = do
     env <- getEnv
@@ -235,14 +227,19 @@
     , typeConstructorsAreEqual env moduleName className' (tcdClassName tcd)
     , subst <- maybeToList $ typeHeadsAreEqual moduleName env ty' (tcdInstanceType tcd)
     , args <- solveSubgoals env subst (tcdDependencies tcd) ]
+  solveSubgoals :: Environment -> [(String, Type)] -> Maybe [(Qualified ProperName, Type)] -> [Maybe [Value]]
   solveSubgoals _ _ Nothing = return Nothing
   solveSubgoals env subst (Just subgoals) = do
     dict <- mapM (go env) (replaceAllTypeVars subst subgoals)
     return $ Just dict
-  mkDictionary fnName args = maybe id (flip App) args $ (Var fnName)
+  mkDictionary :: Qualified Ident -> Maybe [Value] -> Value
+  mkDictionary fnName Nothing = Var fnName
+  mkDictionary fnName (Just dicts) = foldr (flip App) (Var fnName) dicts
+  filterModule :: TypeClassDictionaryInScope -> Bool
   filterModule (TypeClassDictionaryInScope { tcdName = Qualified (Just mn) _ }) | mn == moduleName = True
   filterModule (TypeClassDictionaryInScope { tcdName = Qualified Nothing _ }) = True
   filterModule _ = False
+  canonicalizeDictionary :: TypeClassDictionaryInScope -> Qualified Ident
   canonicalizeDictionary (TypeClassDictionaryInScope { tcdType = TCDRegular, tcdName = nm }) = nm
   canonicalizeDictionary (TypeClassDictionaryInScope { tcdType = TCDAlias nm }) = nm
 
@@ -251,11 +248,7 @@
 -- and return a substitution from type variables to types which makes the type heads unify.
 --
 typeHeadsAreEqual :: ModuleName -> Environment -> Type -> Type -> Maybe [(String, Type)]
-typeHeadsAreEqual _ _ String String = Just []
-typeHeadsAreEqual _ _ Number Number = Just []
-typeHeadsAreEqual _ _ Boolean Boolean = Just []
 typeHeadsAreEqual _ _ (Skolem s1) (Skolem s2) | s1 == s2 = Just []
-typeHeadsAreEqual _ _ Array Array = Just []
 typeHeadsAreEqual m e (TypeConstructor c1) (TypeConstructor c2) | typeConstructorsAreEqual e m c1 c2 = Just []
 typeHeadsAreEqual m e (TypeApp h1 (TypeVar v)) (TypeApp h2 arg) = (:) (v, arg) <$> typeHeadsAreEqual m e h1 h2
 typeHeadsAreEqual m e t1@(TypeApp _ _) t2@(TypeApp _ (TypeVar _)) = typeHeadsAreEqual m e t2 t1
@@ -387,13 +380,13 @@
 -- Infer a type for a value
 --
 infer' :: Value -> UnifyT Check Value
-infer' v@(NumericLiteral _) = return $ TypedValue True v Number
-infer' v@(StringLiteral _) = return $ TypedValue True v String
-infer' v@(BooleanLiteral _) = return $ TypedValue True v Boolean
+infer' v@(NumericLiteral _) = return $ TypedValue True v tyNumber
+infer' v@(StringLiteral _) = return $ TypedValue True v tyString
+infer' v@(BooleanLiteral _) = return $ TypedValue True v tyBoolean
 infer' (ArrayLiteral vals) = do
   ts <- mapM infer vals
   els <- fresh
-  forM_ ts $ \(TypedValue _ _ t) -> els ?= TypeApp Array t
+  forM_ ts $ \(TypedValue _ _ t) -> els ?= TypeApp tyArray t
   return $ TypedValue True (ArrayLiteral ts) els
 infer' (Unary op val) = do
   v <- infer val
@@ -418,9 +411,9 @@
   return $ TypedValue True (ObjectUpdate o' newVals) $ Object $ rowFromList (newTys, row)
 infer' (Indexer index val) = do
   el <- fresh
-  index' <- check index Number
-  val' <- check val (TypeApp Array el)
-  return $ TypedValue True (Indexer (TypedValue True index' Number) (TypedValue True val' (TypeApp Array el))) el
+  index' <- check index tyNumber
+  val' <- check val (TypeApp tyArray el)
+  return $ TypedValue True (Indexer (TypedValue True index' tyNumber) (TypedValue True val' (TypeApp tyArray el))) el
 infer' (Accessor prop val) = do
   typed@(TypedValue _ _ objTy) <- infer val
   propTy <- inferProperty objTy prop
@@ -428,19 +421,19 @@
     Nothing -> do
       field <- fresh
       rest <- fresh
-      objTy `subsumes` Object (RCons prop field rest)
+      _ <- subsumes Nothing objTy (Object (RCons prop field rest))
       return $ TypedValue True (Accessor prop typed) field
     Just ty -> return $ TypedValue True (Accessor prop typed) ty
-infer' (Abs args ret) = do
-  ts <- replicateM (length args) fresh
+infer' (Abs arg ret) = do
+  ty <- fresh
   Just moduleName <- checkCurrentModule <$> get
-  bindLocalVariables moduleName (zip args ts) $ do
+  bindLocalVariables moduleName [(arg, ty)] $ do
     body@(TypedValue _ _ bodyTy) <- infer' ret
-    return $ TypedValue True (Abs args body) $ Function ts bodyTy
-infer' (App f args) = do
+    return $ TypedValue True (Abs arg body) $ function ty bodyTy
+infer' (App f arg) = do
   f'@(TypedValue _ _ ft) <- infer f
   ret <- fresh
-  app <- checkFunctionApplication f' ft args ret
+  app <- checkFunctionApplication f' ft arg ret
   return $ TypedValue True app ret
 infer' (Var var) = do
   Just moduleName <- checkCurrentModule <$> get
@@ -450,7 +443,7 @@
     ConstrainedType constraints _ -> do
       env <- getEnv
       dicts <- getTypeClassDictionaries
-      return $ TypedValue True (App (Var var) (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) ty'
+      return $ TypedValue True (foldl App (Var var) (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) ty'
     _ -> return $ TypedValue True (Var var) ty'
 infer' (Block ss) = do
   ret <- fresh
@@ -470,7 +463,7 @@
   binders' <- checkBinders (map (\(TypedValue _ _ t) -> t) ts) ret binders
   return $ TypedValue True (Case ts binders') ret
 infer' (IfThenElse cond th el) = do
-  cond' <- check cond Boolean
+  cond' <- check cond tyBoolean
   v2@(TypedValue _ _ t2) <- infer th
   v3@(TypedValue _ _ t3) <- infer el
   t2 ?= t3
@@ -525,9 +518,9 @@
 -- Built-in unary operators
 --
 unaryOps :: [(UnaryOperator, (Type, Type))]
-unaryOps = [ (Negate, (Number, Number))
-           , (Not, (Boolean, Boolean))
-           , (BitwiseNot, (Number, Number))
+unaryOps = [ (Negate, (tyNumber, tyNumber))
+           , (Not, (tyBoolean, tyBoolean))
+           , (BitwiseNot, (tyNumber, tyNumber))
            ]
 
 -- |
@@ -536,7 +529,7 @@
 inferBinary :: BinaryOperator -> Value -> Value -> UnifyT Check Value
 inferBinary op left@(TypedValue _ _ leftTy) right@(TypedValue _ _ rightTy) | isEqualityTest op = do
   leftTy ?= rightTy
-  return $ TypedValue True (Binary op left right) Boolean
+  return $ TypedValue True (Binary op left right) tyBoolean
 inferBinary op left@(TypedValue _ _ leftTy) right@(TypedValue _ _ rightTy) =
   case fromMaybe (error "Invalid operator") $ lookup op binaryOps of
     (valTy, resTy) -> do
@@ -550,7 +543,7 @@
 --
 checkBinary :: BinaryOperator -> Value -> Value -> Type -> UnifyT Check Value
 checkBinary op left right res | isEqualityTest op = do
-  res ?= Boolean
+  res ?= tyBoolean
   left'@(TypedValue _ _ t1) <- infer left
   right'@(TypedValue _ _ t2) <- infer right
   t1 ?= t2
@@ -575,24 +568,24 @@
 -- Built-in binary operators
 --
 binaryOps :: [(BinaryOperator, (Type, Type))]
-binaryOps = [ (Add, (Number, Number))
-            , (Subtract, (Number, Number))
-            , (Multiply, (Number, Number))
-            , (Divide, (Number, Number))
-            , (Modulus, (Number, Number))
-            , (BitwiseAnd, (Number, Number))
-            , (BitwiseOr, (Number, Number))
-            , (BitwiseXor, (Number, Number))
-            , (ShiftRight, (Number, Number))
-            , (ZeroFillShiftRight, (Number, Number))
-            , (And, (Boolean, Boolean))
-            , (Or, (Boolean, Boolean))
-            , (Concat, (String, String))
-            , (Modulus, (Number, Number))
-            , (LessThan, (Number, Boolean))
-            , (LessThanOrEqualTo, (Number, Boolean))
-            , (GreaterThan, (Number, Boolean))
-            , (GreaterThanOrEqualTo, (Number, Boolean))
+binaryOps = [ (Add, (tyNumber, tyNumber))
+            , (Subtract, (tyNumber, tyNumber))
+            , (Multiply, (tyNumber, tyNumber))
+            , (Divide, (tyNumber, tyNumber))
+            , (Modulus, (tyNumber, tyNumber))
+            , (BitwiseAnd, (tyNumber, tyNumber))
+            , (BitwiseOr, (tyNumber, tyNumber))
+            , (BitwiseXor, (tyNumber, tyNumber))
+            , (ShiftRight, (tyNumber, tyNumber))
+            , (ZeroFillShiftRight, (tyNumber, tyNumber))
+            , (And, (tyBoolean, tyBoolean))
+            , (Or, (tyBoolean, tyBoolean))
+            , (Concat, (tyString, tyString))
+            , (Modulus, (tyNumber, tyNumber))
+            , (LessThan, (tyNumber, tyBoolean))
+            , (LessThanOrEqualTo, (tyNumber, tyBoolean))
+            , (GreaterThan, (tyNumber, tyBoolean))
+            , (GreaterThanOrEqualTo, (tyNumber, tyBoolean))
             ]
 
 -- |
@@ -600,16 +593,16 @@
 --
 inferBinder :: Type -> Binder -> UnifyT Check (M.Map Ident Type)
 inferBinder _ NullBinder = return M.empty
-inferBinder val (StringBinder _) = val ?= String >> return M.empty
-inferBinder val (NumberBinder _) = val ?= Number >> return M.empty
-inferBinder val (BooleanBinder _) = val ?= Boolean >> return M.empty
+inferBinder val (StringBinder _) = val ?= tyString >> return M.empty
+inferBinder val (NumberBinder _) = val ?= tyNumber >> return M.empty
+inferBinder val (BooleanBinder _) = val ?= tyBoolean >> return M.empty
 inferBinder val (VarBinder name) = return $ M.singleton name val
 inferBinder val (NullaryBinder ctor) = do
   env <- getEnv
   Just moduleName <- checkCurrentModule <$> get
   case M.lookup (qualify moduleName ctor) (dataConstructors env) of
     Just (ty, _) -> do
-      ty `subsumes` val
+      _ <- subsumes Nothing ty val
       return M.empty
     _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"
 inferBinder val (UnaryBinder ctor binder) = do
@@ -619,8 +612,8 @@
     Just (ty, _) -> do
       fn <- replaceAllVarsWithUnknowns ty
       case fn of
-        Function [obj] ret -> do
-          val `subsumes` ret
+        TypeApp (TypeApp t obj) ret | t == tyFunction -> do
+          _ <- subsumes Nothing val ret
           inferBinder obj binder
         _ -> throwError $ "Constructor " ++ show ctor ++ " is not a unary constructor"
     _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"
@@ -641,13 +634,13 @@
 inferBinder val (ArrayBinder binders) = do
   el <- fresh
   m1 <- M.unions <$> mapM (inferBinder el) binders
-  val ?= TypeApp Array el
+  val ?= TypeApp tyArray el
   return m1
 inferBinder val (ConsBinder headBinder tailBinder) = do
   el <- fresh
   m1 <- inferBinder el headBinder
   m2 <- inferBinder val tailBinder
-  val ?= TypeApp Array el
+  val ?= TypeApp tyArray el
   return $ m1 `M.union` m2
 inferBinder val (NamedBinder name binder) = do
   m <- inferBinder val binder
@@ -666,7 +659,7 @@
     case grd of
       Nothing -> return (binders, Nothing, val')
       Just g -> do
-        g' <- check g Boolean
+        g' <- check g tyBoolean
         return (binders, Just g', val')
   rs <- checkBinders nvals ret bs
   return $ r : rs
@@ -698,7 +691,7 @@
     Just ty -> do t ?= ty
                   return (False, mass, Assignment ident val')
 checkStatement mass ret (While val inner) = do
-  val' <- check val Boolean
+  val' <- check val tyBoolean
   (allCodePathsReturn, _, inner') <- checkBlock mass ret inner
   return (allCodePathsReturn, mass, While val' inner')
 checkStatement mass ret (If ifst) = do
@@ -707,9 +700,9 @@
 checkStatement mass ret (For ident start end inner) = do
   Just moduleName <- checkCurrentModule <$> get
   assignVariable ident
-  start' <- check start Number
-  end' <- check end Number
-  (allCodePathsReturn, _, inner') <- bindLocalVariables moduleName [(ident, Number)] $ checkBlock mass ret inner
+  start' <- check start tyNumber
+  end' <- check end tyNumber
+  (allCodePathsReturn, _, inner') <- bindLocalVariables moduleName [(ident, tyNumber)] $ checkBlock mass ret inner
   return (allCodePathsReturn, mass, For ident start' end' inner')
 checkStatement mass ret (Return val) = do
   val' <- check val ret
@@ -720,11 +713,11 @@
 --
 checkIfStatement :: M.Map Ident Type -> Type -> IfStatement -> UnifyT Check (Bool, IfStatement)
 checkIfStatement mass ret (IfStatement val thens Nothing) = do
-  val' <- check val Boolean
+  val' <- check val tyBoolean
   (_, _, thens') <- checkBlock mass ret thens
   return (False, IfStatement val' thens' Nothing)
 checkIfStatement mass ret (IfStatement val thens (Just elses)) = do
-  val' <- check val Boolean
+  val' <- check val tyBoolean
   (allCodePathsReturn1, _, thens') <- checkBlock mass ret thens
   (allCodePathsReturn2, elses') <- checkElseStatement mass ret elses
   return (allCodePathsReturn1 && allCodePathsReturn2, IfStatement val' thens' (Just elses'))
@@ -792,52 +785,56 @@
     TypeClassDictionaryInScope name className instanceTy Nothing TCDRegular) (map (Qualified Nothing) dictNames)
       (qualifyAllUnqualifiedNames moduleName env constraints)) $
         check val ty
-  return $ Abs dictNames val'
+  return $ foldr Abs val' dictNames
 check' val u@(TUnknown _) = do
   val'@(TypedValue _ _ ty) <- infer val
   -- Don't unify an unknown with an inferred polytype
   ty' <- replaceAllVarsWithUnknowns ty
   ty' ?= u
   return val'
-check' v@(NumericLiteral _) Number = return v
-check' v@(StringLiteral _) String = return v
-check' v@(BooleanLiteral _) Boolean = return v
+check' v@(NumericLiteral _) t | t == tyNumber = return v
+check' v@(StringLiteral _) t | t == tyString = return v
+check' v@(BooleanLiteral _) t | t == tyBoolean = return v
 check' (Unary op val) ty = checkUnary op val ty
 check' (Binary op left right) ty = checkBinary op left right ty
-check' (ArrayLiteral vals) (TypeApp Array ty) = ArrayLiteral <$> forM vals (\val -> check val ty)
+check' (ArrayLiteral vals) (TypeApp a ty) | a == tyArray = ArrayLiteral <$> forM vals (\val -> check val ty)
 check' (Indexer index vals) ty = do
-  index' <- check index Number
-  vals' <- check vals (TypeApp Array ty)
+  index' <- check index tyNumber
+  vals' <- check vals (TypeApp tyArray ty)
   return $ Indexer index' vals'
-check' (Abs args ret) (Function argTys retTy) = do
+check' (Abs arg ret) (TypeApp (TypeApp t argTy) retTy) | t == tyFunction = do
   Just moduleName <- checkCurrentModule <$> get
-  guardWith "Incorrect number of function arguments" (length args == length argTys)
-  ret' <- bindLocalVariables moduleName (zip args argTys) $ check ret retTy
-  return $ Abs args ret'
-check' (App f args) ret = do
+  ret' <- bindLocalVariables moduleName [(arg, argTy)] $ check ret retTy
+  return $ Abs arg ret'
+check' (App f arg) ret = do
   f'@(TypedValue _ _ ft) <- infer f
-  app <- checkFunctionApplication f' ft args ret
+  app <- checkFunctionApplication f' ft arg ret
   return $ app
-check' (Var var) ty = do
+check' v@(Var var) ty = do
   Just moduleName <- checkCurrentModule <$> get
   ty1 <- lookupVariable moduleName var
   repl <- replaceAllTypeSynonyms ty1
-  repl `subsumes` ty
-  return $ Var var
+  v' <- subsumes (Just v) repl ty
+  case v' of
+    Nothing -> throwError "Unable to check type subsumption"
+    Just v'' -> return v''
 check' (TypedValue checkType val ty1) ty2 = do
   Just moduleName <- checkCurrentModule <$> get
   kind <- liftCheck $ kindOf moduleName ty1
   guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
-  ty1 `subsumes` ty2
-  val' <- if checkType then check val ty1 else return val
-  return $ TypedValue True val' ty1
+  val' <- subsumes (Just val) ty1 ty2
+  case val' of
+    Nothing -> throwError "Unable to check type subsumption"
+    Just val'' -> do
+      val''' <- if checkType then check val'' ty1 else return val''
+      return $ TypedValue True val''' ty1
 check' (Case vals binders) ret = do
   vals' <- mapM infer vals
   let ts = map (\(TypedValue _ _ t) -> t) vals'
   binders' <- checkBinders ts ret binders
   return $ Case vals' binders'
 check' (IfThenElse cond th el) ty = do
-  cond' <- check cond Boolean
+  cond' <- check cond tyBoolean
   th' <- check th ty
   el' <- check el ty
   return $ IfThenElse cond' th' el'
@@ -869,7 +866,7 @@
     Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"
     Just (ty1, _) -> do
       repl <- replaceAllTypeSynonyms ty1
-      repl `subsumes` ty
+      _ <- subsumes Nothing repl ty
       return $ Constructor c
 check' val (SaturatedTypeSynonym name args) = do
   ty <- expandTypeSynonym name args
@@ -913,49 +910,51 @@
 -- |
 -- Check the type of a function application, rethrowing errors to provide a better error message
 --
-checkFunctionApplication :: Value -> Type -> [Value] -> Type -> UnifyT Check Value
-checkFunctionApplication fn fnTy args ret = rethrow errorMessage $ checkFunctionApplication' fn fnTy args ret
+checkFunctionApplication :: Value -> Type -> Value -> Type -> UnifyT Check Value
+checkFunctionApplication fn fnTy arg ret = rethrow errorMessage $ checkFunctionApplication' fn fnTy arg ret
   where
   errorMessage msg = "Error applying function of type "
     ++ prettyPrintType fnTy
-    ++ " to arguments " ++ intercalate ", " (map prettyPrintValue args)
+    ++ " to argument " ++ prettyPrintValue arg
     ++ ":\n" ++ msg
 
 -- |
 -- Check the type of a function application
 --
-checkFunctionApplication' :: Value -> Type -> [Value] -> Type -> UnifyT Check Value
-checkFunctionApplication' fn (Function argTys retTy) args ret = do
-  guardWith "Incorrect number of function arguments" (length args == length argTys)
-  args' <- zipWithM check args argTys
-  retTy `subsumes` ret
-  return $ App fn args'
-checkFunctionApplication' fn (ForAll ident ty) args ret = do
+checkFunctionApplication' :: Value -> Type -> Value -> Type -> UnifyT Check Value
+checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg ret = do
+  tyFunction' ?= tyFunction
+  arg' <- check arg argTy
+  _ <- subsumes Nothing retTy ret
+  return $ App fn arg'
+checkFunctionApplication' fn (ForAll ident ty) arg ret = do
   replaced <- replaceVarWithUnknown ident ty
-  checkFunctionApplication fn replaced args ret
-checkFunctionApplication' fn u@(TUnknown _) args ret = do
-  args' <- mapM (\arg -> infer arg >>= \(TypedValue _ v t) -> TypedValue True v <$> replaceAllVarsWithUnknowns t) args
-  let tys = map (\(TypedValue _ _ t) -> t) args'
-  u ?= Function tys ret
-  return $ App fn args'
-checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) args ret = do
+  checkFunctionApplication fn replaced arg ret
+checkFunctionApplication' fn u@(TUnknown _) arg ret = do
+  arg' <- do
+    TypedValue _ v t <- infer arg
+    TypedValue True v <$> replaceAllVarsWithUnknowns t
+  let ty = (\(TypedValue _ _ t) -> t) arg'
+  u ?= function ty ret
+  return $ App fn arg'
+checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) arg ret = do
   ty <- expandTypeSynonym name tyArgs
-  checkFunctionApplication fn ty args ret
-checkFunctionApplication' fn (ConstrainedType constraints fnTy) args ret = do
+  checkFunctionApplication fn ty arg ret
+checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg ret = do
   env <- getEnv
   dicts <- getTypeClassDictionaries
   Just moduleName <- checkCurrentModule <$> get
-  checkFunctionApplication' (App fn (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) fnTy args ret
-checkFunctionApplication' _ fnTy args ret = throwError $ "Applying a function of type "
+  checkFunctionApplication' (foldl App fn (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) fnTy arg ret
+checkFunctionApplication' _ fnTy arg ret = throwError $ "Applying a function of type "
   ++ prettyPrintType fnTy
-  ++ " to argument(s) " ++ intercalate ", " (map prettyPrintValue args)
+  ++ " to argument(s) " ++ prettyPrintValue arg
   ++ " does not yield a value of type " ++ prettyPrintType ret ++ "."
 
 -- |
 -- Check whether one type subsumes another, rethrowing errors to provide a better error message
 --
-subsumes :: Type -> Type -> UnifyT Check ()
-subsumes ty1 ty2 = rethrow errorMessage $ subsumes' ty1 ty2
+subsumes :: Maybe Value -> Type -> Type -> UnifyT Check (Maybe Value)
+subsumes val ty1 ty2 = rethrow errorMessage $ subsumes' val ty1 ty2
   where
   errorMessage msg = "Error checking that type "
     ++ prettyPrintType ty1
@@ -966,12 +965,21 @@
 -- |
 -- Check whether one type subsumes another
 --
-subsumes' :: Type -> Type -> UnifyT Check ()
-subsumes' (ForAll ident ty1) ty2 = do
+subsumes' :: Maybe Value -> Type -> Type -> UnifyT Check (Maybe Value)
+subsumes' val (ForAll ident ty1) ty2 = do
   replaced <- replaceVarWithUnknown ident ty1
-  replaced `subsumes` ty2
-subsumes' (Function args1 ret1) (Function args2 ret2) = do
-  zipWithM_ subsumes args2 args1
-  ret1 `subsumes` ret2
-subsumes' ty1 ty2 = ty1 ?= ty2
+  subsumes val replaced ty2
+subsumes' val (TypeApp (TypeApp f1 arg1) ret1) (TypeApp (TypeApp f2 arg2) ret2) | f1 == tyFunction && f2 == tyFunction = do
+  subsumes Nothing arg2 arg1
+  subsumes Nothing ret1 ret2
+  return val
+subsumes' (Just val) (ConstrainedType constraints ty1) ty2 = do
+  env <- getEnv
+  dicts <- getTypeClassDictionaries
+  Just moduleName <- checkCurrentModule <$> get
+  _ <- subsumes' Nothing ty1 ty2
+  return . Just $ foldl App val (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))
+subsumes' val ty1 ty2 = do
+  ty1 ?= ty2
+  return val
 
diff --git a/src/Language/PureScript/Types.hs b/src/Language/PureScript/Types.hs
--- a/src/Language/PureScript/Types.hs
+++ b/src/Language/PureScript/Types.hs
@@ -35,28 +35,8 @@
   -- |
   -- Javascript numbers
   --
-  | Number
-  -- |
-  -- Javascript strings
-  --
-  | String
-  -- |
-  -- Javascript booleans
-  --
-  | Boolean
-  -- |
-  -- Javascript array type constructor
-  --
-  | Array
-  -- |
-  -- Records, parameterized by a row of types
-  --
   | Object Type
   -- |
-  -- A function, with zero or more arguments
-  --
-  | Function [Type] Type
-  -- |
   -- A named type variable
   --
   | TypeVar String
@@ -94,6 +74,42 @@
   | RCons String Type Type deriving (Show, Eq, Data, Typeable)
 
 -- |
+-- Type constructor for functions
+--
+tyFunction :: Type
+tyFunction = TypeConstructor $ (Qualified $ Just $ ModuleName $ ProperName "Prelude") (ProperName "Function")
+
+-- |
+-- Type constructor for strings
+--
+tyString :: Type
+tyString = TypeConstructor $ (Qualified $ Just $ ModuleName $ ProperName "Prelude") (ProperName "String")
+
+-- |
+-- Type constructor for numbers
+--
+tyNumber :: Type
+tyNumber = TypeConstructor $ (Qualified $ Just $ ModuleName $ ProperName "Prelude") (ProperName "Number")
+
+-- |
+-- Type constructor for booleans
+--
+tyBoolean :: Type
+tyBoolean = TypeConstructor $ (Qualified $ Just $ ModuleName $ ProperName "Prelude") (ProperName "Boolean")
+
+-- |
+-- Type constructor for arrays
+--
+tyArray :: Type
+tyArray = TypeConstructor $ (Qualified $ Just $ ModuleName $ ProperName "Prelude") (ProperName "Array")
+
+-- |
+-- Smart constructor for function types
+--
+function :: Type -> Type -> Type
+function t1 t2 = TypeApp (TypeApp tyFunction t1) t2
+
+-- |
 -- Convert a row to a list of pairs of labels and types
 --
 rowToList :: Type -> ([(String, Type)], Type)
@@ -113,18 +129,7 @@
 --
 isMonoType :: Type -> Bool
 isMonoType (ForAll _ _) = False
-isMonoType ty = isPolyType ty
-
--- |
--- Check whather a type is a valid polytype
---
-isPolyType :: Type -> Bool
-isPolyType (Object ps) = all isPolyType (map snd . fst $ rowToList ps)
-isPolyType (Function args ret) = all isPolyType args && isPolyType ret
-isPolyType (TypeApp t1 t2) = isMonoType t1 && isMonoType t2
-isPolyType (SaturatedTypeSynonym _ args) = all isPolyType args
-isPolyType (ForAll _ ty) = isPolyType ty
-isPolyType _ = True
+isMonoType ty = True
 
 -- |
 -- Universally quantify a type
diff --git a/src/Language/PureScript/Values.hs b/src/Language/PureScript/Values.hs
--- a/src/Language/PureScript/Values.hs
+++ b/src/Language/PureScript/Values.hs
@@ -190,11 +190,11 @@
   -- |
   -- Function introduction
   --
-  | Abs [Ident] Value
+  | Abs Ident Value
   -- |
   -- Function application
   --
-  | App Value [Value]
+  | App Value Value
   -- |
   -- Variable
   --