xenophobia

data Nat = Zero | Succ Nat
data SNat (n :: Nat) where
    SZero :: SNat 'Zero
    SSucc :: SNat m -> SNat ('Succ m)

xenophobia

type family NIntArrow (a :: Nat)
type instance NIntArrow 'Zero = Int
type instance NIntArrow ('Succ n) = Int -> NIntArrow 

xenophobia

addN :: SNat nat -> NIntArrow nat
addN n = addN' n 0
    where
      addN' :: SNat nat -> Int -> NIntArrow nat
      addN' SZero acc = acc
      addN' (SSucc n') acc = \x -> addN' n' (acc+x)

xenophobia

{-# Language FlexibleInstances, ScopedTypeVariables #-}
class AddNType t where
    adds :: Int -> t
instance AddNType Int where
    adds = id
instance AddNType t => AddNType (Int -> t) where
    adds n = \m -> (adds (n+m) :: t)

addN :: AddNType t => t
addN = adds 0

xenophobia

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverlappingInstances #-}

import Control.Comonad
import Language.Haskell.Codo

type Option = String

xenophobia

config :: Config
config = [ooLikeSyntax|
           builder <- defaultBuilder
           builder#profile
           builder#goFaster
           builder#extract|]

xenophobia

> (define $onetwo {1 @onetwo 2})
> (test (match onetwo (list integer) {[<join _ _> <Ok>] [_ <Ko>]}))
> <Ok>

xenophobia

import Prelude hiding (head, tail)
import Control.Comonad

data Stream a = St {head :: a, tail :: Stream a}

instance Functor Stream where
    fmap f s = St (f (head s)) (fmap f (tail s))

instance Comonad Stream where
    extract = head

xenophobia

import Prelude hiding (head, tail)
import Control.Comonad

data Stream a = St {head :: a, tail :: Stream a}

instance Functor Stream where
    fmap f s = St (f (head s)) (fmap f (tail s))

instance Comonad Stream where
    extract = head

xenophobia

{- http://d.hatena.ne.jp/majiang/20130602/1370188046 -}
-- return, >>= は所与ってことにする

s :: a        -- 0
ms :: m a        -- 1
f :: a -> b        -- 4
mf :: m (a -> b)        -- 6

f s :: b
return (f s) :: m b