Skip to content

Instantly share code, notes, and snippets.

@LSLeary
LSLeary / LambdaEncodings.md
Last active February 18, 2025 22:19
Scott & Church Encodings

Scott & Church Encodings

Algebraic Data Types

It suffices to describe sums, products and their identities to obtain the full wealth of ADTs:

newtype a + b = Sum{ matchSum :: forall r. (a -> r) -> (b -> r) -> r) }

left :: a -> a + b
@LSLeary
LSLeary / fragment.cabal
Created February 12, 2025 00:47
Structuring a cabal file so as to provide a unified `dev` component.
-- A demonstration, using a fragment of an unpublished library as-is.
-- Split out fields shared by all components into a common stanza:
common shared
build-depends: base
default-language: Haskell2010
default-extensions: ImportQualifiedPost
GeneralisedNewtypeDeriving
DerivingVia
DeriveTraversable
@LSLeary
LSLeary / EventManager.hs
Created January 21, 2025 16:07
A simple, functional event manager.
{-# LANGUAGE RankNTypes, PolyKinds, GeneralisedNewtypeDeriving #-}
module EventManager (
EventManager,
EventTag, eventTag,
attach, trigger,
) where
-- base
import Prelude hiding (lookup)
@LSLeary
LSLeary / HasC.hs
Last active January 15, 2025 02:35
How to write `HasC` as a newtype with a pattern synonym.
{-# LANGUAGE GHC2021, RoleAnnotations, DeriveAnyClass #-}
{-# LANGUAGE UnboxedTuples, PatternSynonyms, ViewPatterns #-}
{- |
This module implements (for empty 'C'):
> data HasC a where
> HasC :: C a => !a -> HasC a
as an opaque newtype with a pattern synonym.
@LSLeary
LSLeary / Coercible.hs
Last active January 5, 2025 10:15
Generalised Coercible
-- These coercions could probably be generated automatically with a
-- type class and this plugin:
-- https://github.com/noughtmare/transitive-constraint-plugin
{-# LANGUAGE UnboxedTuples, UnliftedNewtypes, ExplicitNamespaces #-}
{-# LANGUAGE RoleAnnotations, DataKinds, QuantifiedConstraints #-}
module Coercible (
Coercible(..),
@LSLeary
LSLeary / Yoneda.hs
Last active February 4, 2025 04:00
A more general treatment of the Yoneda lemma than is given in Data.Functor.Yoneda.
{-# LANGUAGE GHC2021, BlockArguments #-}
module Yoneda where
import Prelude hiding (id, (.), map)
import Control.Category
-- Preliminaries
class (Category c, Category d) => ExoFunctor c d f where
{-# LANGUAGE LambdaCase #-}
module Collapse where
-- base
import Data.Functor ((<&>))
import Data.Functor.Classes (Show1)
import Data.Foldable (toList)
import Control.Monad (ap)
@LSLeary
LSLeary / Graded.hs
Last active November 8, 2024 04:36 — forked from axman6/Tracked Exceptions.hs
Checked exceptions implemented by grading IO with the set of exceptions an action may throw.
{-# LANGUAGE DataKinds, TypeFamilies, UndecidableInstances, RoleAnnotations
, QuantifiedConstraints, RebindableSyntax, BlockArguments
, RequiredTypeArguments
#-}
module Graded (
GradedAppl(..), (<*>), (<*), (*>),
GradedAlt(..),
GradedMonad(..), (>>),
@LSLeary
LSLeary / 0-InlineFix.hs
Last active October 3, 2024 22:51
Unrolling recursive functions at static arguments using church numerals
{-# LANGUAGE BlockArguments #-}
module InlineFix (
Rec,
inlineFix,
Church, (|&), _0, _1, _2, _3, _4, _5, _6, _7, _8, _9,
) where
import GHC.Exts (inline)
import Data.Function (fix)
@LSLeary
LSLeary / LeibnizC.hs
Created September 23, 2024 08:06
Leibniz equality as a quantified constraint with safe reification and reflection
{-# LANGUAGE QuantifiedConstraints
, UndecidableInstances
, AllowAmbiguousTypes
#-}
{-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-}
module LeibnizC where
import Leibniz