goldfirere / effects

A Haskell translation of Idris's original algebraic effects library

Haskell translation of Idris's Algebraic Effects Library

This directory contains a translation of the algebraic effects library originally written in Idris for Brady's ICFP 2013 paper, "Programming and Reasoning with Algebraic Effects and Dependent Types". It compiles with a version of GHC 8 that has GHC bug #12442 fixed. This fix is in HEAD, as of this writing.

Files beginning with Sec in this directory correspond to sections in Brady's original paper.

This implementation of algebraic effects is based on the version described in the paper and available here. Note that this version is several years old. Newer versions of this library use higher-rank types in a way not yet available in GHC, though the use case is encompassed by my design for Dependent Haskell.

effects's Issues

SubListProof & ElemProof can be marked injective

Moved from thesis

Type families SubListProof and ElemProof can be made injective, does that help anywhere?

type family
  SubListProof = (res :: SubList (xs :: [a]) (ys :: [a])) | res -> xs a where
  SubListProof = SubNil
  SubListProof = Keep SubListProof
  SubListProof = Drop SubListProof

type family
  ElemProof = (res :: EffElem eff a xs) | res -> eff a xs where
  ElemProof = Here
  ElemProof = There ElemProof