tel

{-# LANGUAGE RankNTypes           #-}

module Edge where

import           Control.Applicative
import           Control.Arrow
import           Control.Category
import           Control.Monad.Morph
import           Control.Monad.State.Strict
import           Pipes.Core

tel

-- Proofs that something is not an element of a vector
using ( x : t, y : t, xs : Vect n t )
  data NElem : t -> Vect n t -> Type where
    Empty : NElem x []
    Miss  : Not (y = x) -> NElem x xs -> NElem x (y :: xs)

namespace Uniq
  -- Vector types where each element is unique
  data Uniq : Nat -> Type -> Type where

tel

module Rel

DecProofType : {a:Type} -> Dec a -> Type
DecProofType {a} (Yes _)  = a
DecProofType {a} (No _)   = a -> _|_
 
decProof : {a:Type} -> (dec : Dec a) -> DecProofType dec
decProof (Yes x)  = x
decProof (No x)   = x

tel

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RankNTypes        #-}
{-# LANGUAGE TypeFamilies      #-}

module Dbs where

import           Control.Monad.Morph
import           Control.Monad.ST         (RealWorld, ST, runST, stToIO)
import           Control.Monad.Trans.Free
import           Data.Array.ST

tel

{-# LANGUAGE Arrows                #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell       #-}

module Ex where

import           Control.Applicative
import           Control.Arrow

tel

instance Monoid Bool where
  mempty = True
  x <> y = x == y

[ mempty <> x == x ]
True <> True  == True
True <> False == False

[ x <> mempty == x ]
-- dispatched by symmetry of (==)

tel

protocol Viewl {
    typealias El
    func uncons() -> (El, Self)?
}

func head<X:Viewl>(x: X) -> X.El? { return x.uncons()?.0 }
func tail<X:Viewl>(x: X) -> X?    { return x.uncons()?.1 }

extension String:Viewl {
    typealias El = Character

tel

func id  <A>(a: A)      -> A { return a }
func fix <A>(f: A -> A) -> A { return f(fix(f)) }
func loop<A>()          -> A { return fix(id) }

protocol Viewl {
    typealias El
    func uncons() -> (El, Self)?
}

func head<X:Viewl>(x: X) -> X.El? { return x.uncons()?.0 }

tel

enum Maybe<A> {
    case Nothing, Just(A)
    
    func map<B> (f: A -> B) -> Maybe<B> {
        switch self {
        case .Nothing: return .Nothing
        case .Just(let a): return .Just(f(a))
        }
    }
    

tel

{-# LANGUAGE DeriveFoldable    #-}
{-# LANGUAGE DeriveFunctor     #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE TypeFamilies      #-}

module Bin where

import           Control.Applicative
import qualified Data.Foldable       as F