Skip to content

Instantly share code, notes, and snippets.

View bolt12's full-sized avatar
🆓
Free them all

Armando Santos bolt12

🆓
Free them all
121 followers · 217 following
View GitHub Profile
@bolt12
bolt12 / scoped-effects-notes-2020-11-12.md
Created November 13, 2020 04:45 — forked from lexi-lambda/scoped-effects-notes-2020-11-12.md

With scoped effects, handlers must be a part of the program

It is seductive to imagine that effect handlers in an algebraic effect system are not part of the program itself but metalanguage-level folds over the program tree. And in traditional free-like formulations, this is in fact the case. The Eff monad represents the program tree, which has only two cases:

data Eff effs a where
  Pure :: a -> Eff effs a
  Op :: Op effs a -> (a -> Eff effs b) -> Eff effs b

data Op effs a where
@bolt12
bolt12 / StackDD.hs
Created August 17, 2020 18:38
Denotational Design of a Stack API
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE LambdaCase #-}
module DD where
newtype Stack a = S (Int -> a)
empty :: Stack a
empty = S (\case {})
@bolt12
bolt12 / DD.hs
Created August 7, 2020 07:46
Denotational Design Experiment
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module DD where
import Data.Functor.Compose
import Data.Monoid
newtype TMap k v = TM (k -> v)
type Map k v = Compose (TMap k) First v
@bolt12
bolt12 / LiquidRel.hs
Created April 18, 2020 13:55
Liquid Haskell Relational Specification with inductive matrix data type and linear map semantics.
{-@ LIQUID "--no-totality" @-}
{-@ LIQUID "--no-termination" @-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
@bolt12
bolt12 / SelectiveProb.hs
Last active April 10, 2020 10:31
Probabilistic Programming using Free Selective Functors let us statically analyse which effects are necessary.
{-# LANGUAGE GADTs #-}
module SelectiveProb where
import Control.Selective.Free
import Control.Selective
import System.Random.MWC
import System.Random.MWC.Distributions
import Data.Bool
import Data.Bifunctor (bimap)
import qualified Data.Vector as V
@bolt12
bolt12 / AllValuesPolished.hs
Created March 24, 2020 20:41
All possible inhabitants of a given type
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NoStarIsType #-}
@bolt12
bolt12 / AllValues.hs
Last active March 24, 2020 17:35
All possible inhabitants of a given type
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE TypeFamilies #-}
@bolt12
bolt12 / CpBibs.txt
Created May 2, 2017 18:39
Bibliotecas de CP
http://wiki.di.uminho.pt/twiki/pub/Education/CP/MaterialPedagogico/Cp.hs
http://wiki.di.uminho.pt/twiki/pub/Education/CP/MaterialPedagogico/Probability.hs
http://wiki.di.uminho.pt/twiki/pub/Education/CP/MaterialPedagogico/ListUtils.hs
http://wiki.di.uminho.pt/twiki/pub/Education/CP/MaterialPedagogico/Show.hs
http://wiki.di.uminho.pt/twiki/pub/Education/CP/MaterialPedagogico/St.hs
http://wiki.di.uminho.pt/twiki/pub/Education/CP/MaterialPedagogico/Exp.hs
http://wiki.di.uminho.pt/twiki/pub/Education/CP/MaterialPedagogico/FTree.hs
http://wiki.di.uminho.pt/twiki/pub/Education/CP/MaterialPedagogico/LTree.hs
http://wiki.di.uminho.pt/twiki/pub/Education/CP/MaterialPedagogico/BTree.hs
http://wiki.di.uminho.pt/twiki/pub/Education/CP/MaterialPedagogico/List.hs