LSLeary

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

-- 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

{-# LANGUAGE RankNTypes, PolyKinds, GeneralisedNewtypeDeriving #-}

module EventManager (
  EventManager,
  EventTag, eventTag,
  attach, trigger,
) where

-- base
import Prelude hiding (lookup)

LSLeary

{-# 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

-- 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

{-# 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

LSLeary

{-# LANGUAGE LambdaCase #-}

module Collapse where

-- base
import Data.Functor ((<&>))
import Data.Functor.Classes (Show1)
import Data.Foldable (toList)
import Control.Monad (ap)

LSLeary

{-# LANGUAGE DataKinds, TypeFamilies, UndecidableInstances, RoleAnnotations
           , QuantifiedConstraints, RebindableSyntax, BlockArguments
           , RequiredTypeArguments
#-}

module Graded (

  GradedAppl(..), (<*>), (<*), (*>),
  GradedAlt(..),
  GradedMonad(..), (>>),

LSLeary

{-# 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

{-# LANGUAGE QuantifiedConstraints
           , UndecidableInstances
           , AllowAmbiguousTypes
#-}
{-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-}

module LeibnizC where

import Leibniz