LSLeary

{-#
LANGUAGE
  LambdaCase, RoleAnnotations, OverloadedStrings, DerivingStrategies
#-}

module Poheap (
  Poset(..), Prefix(..),
  Poheap, empty, singleton, (<+>),
  pop, assocs,
) where

LSLeary

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

module Phases (Phases, runPhases, phase) where

-- To maintain the heap invariant according to @Ord k@, the type role of @k@
-- must be nominal, and @Phases@ must be opaque.
type role Phases nominal representational representational
data Phases k f a where
  Pure  :: a -> Phases k f a
  Phase :: k -> (w -> x -> y -> z) -> f w -> Phases k f x -> Phases k f y

LSLeary

GADTs That Can Be Newtypes and How to Roll 'Em

I think many people know about Data.Some.Newtype⁠—⁠it uses quite a cute (and cursed) trick to encode a simple existential wrapper as a newtype, hence avoiding an unwanted indirection in the runtime representation.

But there's more to data than existentials⁠—⁠so how far do these tricks go? The answer is: surprisingly far! Let's see what other GADTs we can slim down.

Preliminaries

LSLeary

{-# LANGUAGE GHC2021, RoleAnnotations #-}

module ID (
  ID, newID,
  sameID,
) where

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

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

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