Skip to content

Instantly share code, notes, and snippets.

✍️

Joseph Abrahamson tel

✍️
Block or report user

Report or block tel

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
View Edge.hs
{-# 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
View Rel.idr
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
View Rel.idr
-- 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
View Dbs.hs
{-# 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
View Ex.hs
{-# LANGUAGE Arrows #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell #-}
module Ex where
import Control.Applicative
import Control.Arrow
View gist:9070be588f9cb159ee14
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
tel / left-view
Last active Aug 29, 2015
Left-view enumerations of Swift Strings
View left-view
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
tel / PC.swift
Last active Aug 29, 2015
Swift Compilation Segfault
View PC.swift
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 }
View gist:8e7627e1bce8c5d356f4
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
tel / ComonadZip.hs
Created Aug 22, 2014
Some kind of exploration of comonads and zippers in Binary, non-empty trees
View ComonadZip.hs
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
module Bin where
import Control.Applicative
import qualified Data.Foldable as F
You can’t perform that action at this time.