I wrote most of the type checker for Zaphod back in May, then dropped the project until taking it up again for the Jam at the beginning of August (see commit history).
While I did most of my coding in emacs, I did play with the repl.it environment enough to get Haskell compiling and running.
Zaphod
A two headed language
How is Zaphod a two headed language? In several ways:
Zaphod is like Scheme with Haskell's type system[1] bolted on
Zaphod's type system includes an explicit Top type, so "untyped" functions and macros are possible
[todo] Zaphod supports an alternative syntax that looks much more like Python
Why does Zaphod exist?
Dual foundation
Haskell's type system is great, but metaprogramming with Template Haskell is clunky. Scheme has a great metaprogramming via macros, but is untyped. Zaphod combines the two, with a powerful type system for normal programming and macros for metaprogramming.
Dual syntax [todo]
Lisps are great for manipulating ASTs, but many programmers do not enjoy the parenthesis heavy syntax. Python has a nice, clean syntax, but is clunky for AST manipulations. Zaphod uses the same AST for both Scheme and Python syntaxes, so code can be written with Python syntax while AST manipulations (macros) can be written with Scheme syntax.
What does Zaphod look like?
Basics
;; line comments
(* block
comment *)
;; the unit value
()
;; a (quoted) symbol
'zaphod
;; a tuple of three symbols - the following 4 produce the same value
['a 'b 'c]
(tuple 'a 'b 'c)
(cons 'a (cons 'b (cons c ())))
'(a b c)
;; a lambda expression
(lambda (x) [x x])
Types
() ;; the unit type
Symbol ;; the type for symbols
Top ;; universal return type
(x . y) ;; pair type
;; tuple types, the following two are equivalent
[x y z]
(x . (y . (z . ())))
;; function types, eg, a function from one symbol to another symbol
(-> [Symbol] Symbol)
;; universal quantification, for parametric polymorphism
(forall a (-> [a] a)) ;; the type of the identity function
;; hard to demonstrate, but symbols can also be types, eg, the type 'Bool
Defining a value
;; Explicit type
(def name
Symbol
'Zaphod)
;; Inferred type
(def unit ())
Defining a function
(defn (id x)
(forall a (-> [a] a))
x)
Macros
(def defn
(-> [(Symbol . Top) Type Top] Top)
(macro (p t e)
['def (car p) t ['lambda (cdr p) e]]))
ADTs
(data Bool
True
False)
(data (Maybe a)
Nothing
(Just a))
(defn (not p)
(-> [Bool] Bool)
(if p
False
True))
Why is Zaphod interesting?
Zaphod takes the minimalism of Scheme and applies it to Haskell's type system. Take the data "special form" is not a special form at all, but a macro! Bool is a symbol masquerading as a type, and Maybe is a function from a type to tuple type. True, False and Nil are all symbols that have had their types overwritten, and (Just x) is, similarly a coerced tuple.
Consider Haskell's maybe function. Normally, we would implement this with pattern matching, but Zaphod doesn't have pattern matching yet, so we can abuse the underlying representation.
(defn (maybe d f m)
(forall a (forall b (-> [b
(-> [a] b)
(Maybe a)]
b)))
(if (is-symbol m)
d
(f (unsafe-coerce (cadr m)))))
Future work
Records (via a macro)
Type classes (via macros, after adding implicit arguments)
Numeric, string, character types
References
<a id="1">[1]</a> Dunfield, Joshua, and Neelakantan R. Krishnaswami. “Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism.” Proceedings of the 18th ACM SIGPLAN international conference on Functional programming - ICFP ’13 (2013): n. pag. Crossref. Web.
If you're interested in Haskell-meets-Lisp, Kadena's Pact might be of interest. I haven't played around with it (it's for blockchain applications), but it's an example of combining type systems with macros.
Zaphod programming language
Team: zaph0d
Source: github
Disclosures:
Zaphod
A two headed language
How is Zaphod a two headed language? In several ways:
Top
type, so "untyped"functions and macros are possible
like Python
Why does Zaphod exist?
Dual foundation
Haskell's type system is great, but metaprogramming with Template
Haskell is clunky. Scheme has a great metaprogramming via macros, but
is untyped. Zaphod combines the two, with a powerful type system for
normal programming and macros for metaprogramming.
Dual syntax [todo]
Lisps are great for manipulating ASTs, but many programmers do not
enjoy the parenthesis heavy syntax. Python has a nice, clean syntax,
but is clunky for AST manipulations. Zaphod uses the same AST for
both Scheme and Python syntaxes, so code can be written with Python
syntax while AST manipulations (macros) can be written with Scheme
syntax.
What does Zaphod look like?
Basics
Types
Defining a value
Defining a function
Macros
ADTs
Why is Zaphod interesting?
Zaphod takes the minimalism of Scheme and applies it to Haskell's type
system. Take the
data
"special form" is not a special form at all,but a macro!
Bool
is a symbol masquerading as a type, andMaybe
is a function from a type to tuple type.
True
,False
andNil
are all symbols that have had their types overwritten, and
(Just x)
is, similarly a coerced tuple.
Consider Haskell's
maybe
function. Normally, we would implement this with pattern matching,
but Zaphod doesn't have pattern matching yet, so we can abuse the
underlying representation.
Future work
References
<a id="1">[1]</a>
Dunfield, Joshua, and Neelakantan R. Krishnaswami. “Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism.” Proceedings of the 18th ACM SIGPLAN international conference on Functional programming - ICFP ’13 (2013): n. pag. Crossref. Web.
If you're interested in Haskell-meets-Lisp, Kadena's Pact might be of interest. I haven't played around with it (it's for blockchain applications), but it's an example of combining type systems with macros.