startling

Ok, modules loaded: Main, Language.Coatl.Abstract, Language.Coatl.Parser.Expression, Language.Coatl.Parser.Declaration, Language.Coatl.Graph, Language.Coatl.Check, Language.Coatl.Check.Types.
*Main> main

Language.Coatl.Parser.Expression
  expression
    - parses names
    - parses operators
    - parses infix operators
    - parses lambdas
    - parses the type of the identity function

startling

-- | Some functions on directed graphs.
module Language.Coatl.Graph where
-- base
import Data.Maybe
-- containers
import Data.Map (Map)
import qualified Data.Map as M
import Data.Set (Set)
import qualified Data.Set as S
-- mtl

startling

[ import = [ internal ]
, module = small-example
, pragma = no-prelude
, doc    = "A small example module!"
]

id _ x = x
[ doc  = "The identity function"
, type = dependent type (\a -> function a a)
]

startling

module Control.Applicative.Recipes where
-- base
import Control.Applicative
import Data.Foldable
import Data.Traversable
import Data.Monoid
-- containers
import Data.Set

data Recipe k v m a = Recipe

startling

def bit_iter(bits, n):
    "Iterate over the bits of an integer, padding it to `n` digits."
    return ((bits >> i) & 1 for i in xrange(n - 1, -1, -1))

def unsigned_bin(x, n=32):
    "Print the unsigned binary representation of an integer."
    return "".join(repr(y) for y in bit_iter(x, n))
    

print unsigned_bin(0b101, 8) # '00000101'

startling

import Sheets
import Control.Applicative
import Control.Monad.State
import Data.Text (Text)
import qualified Data.Text as T
import qualified Data.Text.IO as T

simple :: [T.Text] -> Table (State Int) Text
simple = Table [counter id, see]

startling

data MaybeT : (Type -> Type) -> Type where
  MT : {m : Type -> Type} -> m (Maybe a) -> MaybeT m a

startling

def multidecorator(fn):
    class _MultiDecorator(object):
        class __metaclass__(type):
            def __new__(cls, name, bases, dict):
                # No magic on the first class with this metaclass
                if bases == (object,):
                    return type.__new__(cls, fn.__name__, bases, dict)
                else:
                    return fn(**dict)
    return _MultiDecorator

startling

\begin{diagram}
  \named{a}    \box     \box \\
  \box         \box     \named{b} \\
  \box         \box     \empty
\end{diagram}

startling

Elaborating {__Infer0}
builtin:0
---> Type a
builtin:0:Constructor {__infer0} : {{A0} : Type} -> ({a0} : {A0}) -> {__Infer0}
Rechecking ({A0} : Type 0) -> {A0} -> {__Infer0}
---> {__infer0} : ({A0} : Type c) -> {A0} -> {__Infer0}
Forced: {__infer0} []
   from ({A0} : Type c) -> {A0} -> {__Infer0}
Elaborating {__Unit0}
builtin:0