Titan is an experimental type checker implementation written in Haskell.
This implementation is based on the implementation of Typing Haskell in Haskell type checker. I'm going to implement some additional features like:
- Parsers
- Pretty-printers
- Implicit universal quantification
- Kind inference
- Explicit kind signatures and scoped type variables
- Multi-parameter type classes
- Pattern exhaustiveness/useless checker
- Functional dependencies
- Extensible records (row polymorphism)
- Extensible effects
// comment
/* comment */
_a // var (internal)
* // types of values
? // constraints
# k // row kind
k -> k // function kind
_a // var (internal)
Int // con
(->) // con (arrow)
{_} // con (record)
<> // con (empty row)
<+l> // con (row extension)
Pair a b // app
a // quantified var
// syntax sugar
a -> b // is equivalent to (->) a b
{ a } // is equivalent to {_} a
{ ... } // is equivalent to {_} <...>, if possible
<l : a> // is equivalent to <+l> a <>
<l : a | r> // is equivalent to <+l> a r
<l : a, ...> // is equivalent to <+l> a <...>
(a, b, ...) // is equivalent to { 0: a, 1: b, ... }
Coercible a b // class consraints
(c, c) // set of constraints
// type variables are implicitly quantified
a -> f a where Applicative f
// specifying quantification explicitly
[a f] a -> f a where Applicative f
// specifying quantification with kind signatures
[(a : *) (f : * -> *)] a -> f a where Applicative f
123 // integer
'a' // char
3.14 // float
"hello" // string
x // var
x@p // as var
_ // wildcard
Pair a b // decon
123 // lit
x // var
Pair // con
{} // con (empty record)
{.l} // con (record selection)
{-l} // con (record restriction)
{+l} // con (record extension)
{%l} // con (record updation)
Pair a b // app
123 // lit
let id = e, id = e in e // let
fun pats -> e | pats -> e // lam
// syntax sugar
r.l // is equivalent to {.l} r
{ l = a } // is equivalent to {+l} a {}
{ l = a, ... } // is equivalent to {+l} a { ... }
%{ l = a } r // is equivalent to {%l} a r
%{ l = a, ... } r // is equivalent to {%l} a (%{ ... } r)
(a, b, ...) // is equivalent to { 0 = a, 1 = b, ... }
// explicitly typed def
val id : ts
val id : ts = e
// implicitly typed def
val id = e
// data type
data List a {
con Cons a (List a)
con Nil
}
// type class
class Eq a {
val eq : a -> a -> Bool
}
class Ord a where Eq a {
val compare : a -> a -> Ordering
}
class MonadState s m | m ~> s where Monad m {
val get : m s
val put : s -> m ()
}
// instance
instance Eq (Pair a b) where (Eq a, Eq b)
// default
default {
Maybe
Integer
}
// dump
dump(type) val id = fun x -> x
dump(kind) data Free f a {
con Pure a
con Free (f (Free f a))
}