AndrasKovacs

{-# LANGUAGE LambdaCase, DeriveFunctor #-}

import Prelude hiding (take, head)
import Control.Monad
import Control.Monad.Trans

data ListT' m a = Nil | Cons a (ListT m a) deriving (Functor)
newtype ListT m a = ListT {runListT :: m (ListT' m a)} deriving (Functor)

instance Monad m => Monad (ListT m) where

AndrasKovacs

{-# LANGUAGE 
    LambdaCase, DeriveFunctor, FlexibleContexts, 
    RankNTypes, TemplateHaskell, NoMonomorphismRestriction #-}

-- golfing the state monad with free

import Control.Monad
import Control.Monad.Free
import Control.Monad.Free.TH
 

AndrasKovacs

{-# LANGUAGE 
    TemplateHaskell, LambdaCase, MultiParamTypeClasses, 
    FlexibleInstances, FunctionalDependencies #-}

import Control.Applicative
import Control.Lens
import Control.Lens.Extras

data Item = Simple   {_sellIn :: Int, _quality :: Int, _itemName :: String}
          | Conjured {_sellIn :: Int, _quality :: Int, _itemName :: String}

AndrasKovacs

{-# LANGUAGE 
    DataKinds, GADTs, TypeFamilies,
    ScopedTypeVariables, LambdaCase, 
    TemplateHaskell, StandaloneDeriving,
    DeriveFunctor, DeriveFoldable, DeriveTraversable, TypeOperators #-}

import Data.Singletons.TH
import Data.Foldable (Foldable)
import Data.Traversable (Traversable)

AndrasKovacs

{-# LANGUAGE
    DataKinds, PolyKinds, TypeFamilies, TemplateHaskell,
    ScopedTypeVariables, UndecidableInstances, GADTs, TypeOperators #-}

import Data.Singletons.TH

$(singletons [d|
    data Nat = Zero | Succ Nat

    (+) :: Nat -> Nat -> Nat

AndrasKovacs

{-# LANGUAGE MagicHash, UnboxedTuples #-}

import Criterion.Main
import Criterion.Config
import GHC.Exts
import GHC.ST

data Array a = Array (Array# a)

snoc :: Array a -> a -> Array a

AndrasKovacs

open import Function
open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Data.Nat.Properties.Simple
open import Data.Unit

data Bin : Set where
  zero : Bin
  2*n 2*n+1 : Bin → Bin

AndrasKovacs

open import Data.List 
open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Algebra
module LM {a}{A : Set a} = Monoid (monoid A)

infixr 5 _>>=_
_>>=_ : ∀ {a b}{A : Set a}{B : Set b} → List A → (A → List B) → List B

AndrasKovacs

{-# LANGUAGE
    FlexibleInstances, 
    MultiParamTypeClasses, 
    UndecidableInstances, 
    IncoherentInstances, -- GHC 7.10 can do with only Overlapping
    TypeFamilies #-}

class ZipWithN f t where
    zipWithN' :: [f] -> t 

AndrasKovacs

-- Lens style ----------------------

-- Kudos for circed for holes and contexts in lens-style: http://stackoverflow.com/questions/25393870/how-can-holes-and-contexts-be-implemented-for-higher-kinded-types-in-a-lens-styl 


{-# LANGUAGE GADTs, RankNTypes, PolyKinds, StandaloneDeriving, ScopedTypeVariables #-}

import Control.Applicative
import Control.Monad.Identity