startling

-- Because this hasn't reached the prelude yet.
instance Monad (Either x) where
  return = Right
  (Left a) >>= _ = Left a
  (Right a) >>= f = f a

-- In the lambda calculus, expressions are either symbols,
-- function definitions, or applications thereof.
data Expression : Set where
  symbol  : String -> Expression

startling

class Set(object):
    """Sets can contain anything, including themselves. This leads to
    paradoxical behavior: given R, the set of all sets that don't contain
    themselves, does R contain R? Here this becomes an infinite recursion.
    """
    def __init__(self, predicate):
        self.predicate = predicate

    def __contains__(self, obj):
        return self.predicate(obj)

startling

#!/bin/sh

# udhcpc config script

# $interface is the name of the device udhcpc is using
# $router is the (space_separated) list of gateways
# $broadcast is the broadcast address
# $ip is the ip address that we get from the dhcp server
# $dns is the list of dns servers we get from the dhcp server
# $domain is the domain of the network

startling

#!/usr/bin/env sh
# USAGE: ./backup [texts] [pictures] [downloads]
# You can put other files you'd like to back up in $FILES

# Things to remember.
TEXTS="/data/data/com.android.providers.telephony/databases/mmssms.db"
PICTURES="/mnt/sdcard/DCIM/ /mnt/sdcard/Pictures/"
DOWNLOADS="/mnt/sdcard/Download/"

# Parse args.

startling

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
-- base
import Data.List
import Data.Monoid
import Data.Foldable (Foldable)
import Data.Traversable (Traversable)
import Control.Applicative

startling

public final class Nat {
  private final Nat predecessor;

  private Nat (Nat n) {
    predecessor = null;
  }

  public static Nat S(Nat n) {
    return new Nat(n);
  }

startling

data Even : Nat -> Type where
  zeroIsEven : Even O
  evenPlusTwoIsEven : Even k -> Even (k + 2)

twoIsEven : Even 2
twoIsEven = evenPlusTwoIsEven zeroIsEven

threeIsn'tEven : Even 3 -> _|_
threeIsn'tEven zeroIsEven impossible
threeIsn'tEven (evenPlusTwoIsEven n) impossible

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)
]