Skip to content

Instantly share code, notes, and snippets.

@Cedev
Cedev / hklist.hs
Created September 12, 2017 15:06
Heterogenous list (product) that applies a type
{-# LANGUAGE PolyKinds, DataKinds, GADTs, TypeOperators, ConstraintKinds, RankNTypes, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}
import Data.Proxy
import Data.Functor.Identity
import GHC.Exts (Constraint)
data HKList :: (k -> *) -> [k] -> * where
Nil :: HKList f '[]
(:*) :: f x -> HKList f xs -> HKList f (x ': xs)
@Cedev
Cedev / structrally-free-alternative.hs
Created August 13, 2017 02:12
structurally correct free alternative
{-# Language GADTs #-}
{-# Language DataKinds #-}
{-# Language KindSignatures #-}
{-# Language ViewPatterns #-}
{-# Language RankNTypes #-}
{-# Language ScopedTypeVariables #-}
import Control.Applicative
@Cedev
Cedev / tape.hs
Created July 19, 2017 01:28
tape comonad
{-# language DeriveFunctor #-}
{-# language FlexibleInstances #-}
import Data.Function
class Functor w => Comonad w where
extract :: w a -> a
duplicate :: w a -> w (w a)
kfix :: ComonadApply w => w (w a -> a) -> w a
@Cedev
Cedev / nested dos.hs
Created April 16, 2017 05:07
nested dos
main = do
chars <- getLine
let otherchars = do
a <- chars
b <- chars
[a] ++ [b]
putStrLn otherchars
@Cedev
Cedev / structuralEquality.hs
Created September 21, 2015 03:58
Generic typeclass machinery to reason about functors ignoring their arguments
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DeriveGeneric #-} -- Only needed for the DSL example
import GHC.Generics
-- Data types that are constant and uninteresting
class Eq a => Const a
@Cedev
Cedev / TypeMap.hs
Created September 15, 2015 03:00
A map from types to values indexed by those types
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
module Data.TypeMap (
TypeMap (),
null,
size,
member,
deleteLast :: (a -> Bool) -> [a] -> [a]
deleteLast delete = snd . go
where
go [] = (False, [])
go (x:xs) = (delete x || deleteLater, if not (delete x) || deleteLater then x:xs' else xs')
where
(deleteLater, xs') = go xs
filterLast p = deleteLast (not . p)
@Cedev
Cedev / distributions.hs
Created April 10, 2015 18:18
Calculate some interesting statistics about how hard it is to prove that dice aren't the normal distribution
import Statistics.Distribution
import Statistics.Distribution.Normal
data D n = D {n :: n, s :: n}
instance Integral n => Distribution (D n) where
cumulative d x = cumulativeD d (floor x)
instance Integral n => DiscreteDistr (D n) where
probability d x = probabilityD d (fromIntegral x)
import Control.Applicative
import Data.List
import Data.Maybe
data Term = Var Int | Lam Int Term | App Term Term deriving (Show)
data BTerm = BVar Int | BLam BTerm | BApp BTerm BTerm deriving (Show) -- BVar 0 refers to the closest lambda
lam2db :: Term -> Maybe BTerm
lam2db = go []
where
@Cedev
Cedev / Control.PrimRec.hs
Last active August 29, 2015 14:13
Compiler from ArrowLike interface for primitive recursive functions to LLVM
module Control.PrimRec (
ArrowLike (..),
PrimRec (..),
module Control.Category,
module Data.Nat
) where
import Control.Category
import Data.Nat