Skip to content

Latest commit

 

History

History
171 lines (141 loc) · 3.98 KB

README.md

File metadata and controls

171 lines (141 loc) · 3.98 KB
Raw

Titan

Titan is an experimental type checker implementation written in Haskell.

Features

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

Syntax overview

Comments

// comment
/* comment */

Kinds

_a            // var (internal)
*             // types of values
?             // constraints
# k           // row kind
k -> k        // function kind

Types

_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, ... }

Constraints

Coercible a b // class consraints
(c, c)        // set of constraints

Type schemes

// 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

Literals

123           // integer
'a'           // char
3.14          // float
"hello"       // string

Patterns

x             // var
x@p           // as var
_             // wildcard
Pair a b      // decon
123           // lit

Expressions

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, ... }

Declarations

// 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))
}

References