LSLeary

{-# LANGUAGE GHC2021, RoleAnnotations #-}

module ID (
  ID, newID,
  sameID,
) where

-- base
import Unsafe.Coerce (unsafeCoerce)
import Data.Coerce (coerce)

LSLeary

{-# LANGUAGE GHC2021, PatternSynonyms, ViewPatterns, UnboxedTuples #-}
{-# LANGUAGE RoleAnnotations, DataKinds, GADTs #-}

{- |
This module implements

> type Uncurry :: (k1 -> k2 -> Type) -> (k1, k2) -> Type
> data Uncurry f t where
>   UC :: !(f a b) -> Uncurry f '(a, b)

LSLeary

{-# LANGUAGE GHC2021, BlockArguments, LambdaCase #-}

module Search (search) where

search :: Foldable f => (a -> Bool) -> f a -> Maybe a
search p = try . foldMap \x -> if p x
  then Succeed x
  else Fail

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)