Skip to content

Instantly share code, notes, and snippets.

View raichoo's full-sized avatar

raichoo raichoo

View GitHub Profile
@raichoo
raichoo / PlusZero.hs
Last active May 10, 2016 20:19
Oh… this works.
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
module PlusZero where
import Data.Type.Equality
data Nat
= Zero
module Main where
import Prelude
import Control.Monad.Eff
import Control.Monad.Eff.Console
import Debug.Trace
import Data.Maybe
@raichoo
raichoo / anacata.hs
Last active April 7, 2016 13:44
Folding/Unfolding
{-# LANGUAGE NPlusKPatterns #-}
module Main where
import Test.QuickCheck
data NatF a
= ZeroF
| SuccF a
instance Functor NatF where
@raichoo
raichoo / compare.ts
Last active February 24, 2016 19:15
Staring into the abyss of ===. TypeScript edition.
// Whenever I complain about == in JS people always tell me
// that I should use ===, as if that would make more sense.
// the `sel` function takes three values of type A
// we know nothing about, therefore we should not
// be able to compute anything with these values,
// the only thing we should be able to do is
// to constantly return one of them, their
// value should not be able to influence the
// result in any way.
@raichoo
raichoo / semantickata.hs
Last active January 20, 2016 01:26
Mini programming language to implement the recursive `fact` function.
{-# LANGUAGE LambdaCase #-}
module Main where
import Control.Applicative (liftA2)
import Control.Monad.Reader
type Varname = String
type Env = [(Varname, Dom)]
data Dom
@raichoo
raichoo / script.hs
Last active January 19, 2016 07:41
Example why you should avoid unsafe functions like `read`, or at least be careful.
#!/usr/bin/env runhaskell
-- run as script to get correct buffering behavior
-- >>> chmod +x ./script.hs
-- >>> ./script.hs
module Main where
import Control.Exception
example :: IO Int
example =
{-# OPTIONS_GHC -O2 #-}
{-# LANGUAGE OverloadedStrings #-}
module Main where
import System.IO
import Text.Regex.PCRE
import Text.Regex.PCRE.ByteString.Lazy
import Data.Maybe (mapMaybe)
import Data.Char (ord)
import Data.Word (Word8)
@raichoo
raichoo / length.hs
Last active December 19, 2015 20:22
Where the new type of length makes sense.
module Main where
import Data.Foldable (traverse_)
import Text.Printf
printThat x = do
printf "Now printing %d elements\n" (length x)
traverse_ putStrLn x
main = do
@raichoo
raichoo / freet.hs
Last active December 9, 2015 07:10
Playing with `FreeT`
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
module Main where
import Control.Monad.Trans.Free
import Control.Monad.State
import Control.Monad.IO.Class (liftIO)
import System.IO (hFlush, stdout)
@raichoo
raichoo / Codensity.idr
Created September 11, 2015 19:13
List Codensity transformation in Idris
module Main
data Free : (f : Type -> Type) -> (a : Type) -> Type where
Pure : a -> Free f a
Bind : f (Free f a) -> Free f a
instance Functor f => Functor (Free f) where
map f (Pure x) = Pure (f x)
map f (Bind x) = assert_total (Bind (map (map f) x))