Leary 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

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


	module Help (helpAt) where

	-- containers
	import Data.Map.Strict (Map, (!))
	import Data.Map.Strict qualified as M

	-- xmonad
	import XMonad hiding ((\|\|\|))

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

	module Enumeration (
	Enumeration(..),
	fromFoldable,
	) where

	-- GHC/base
	import GHC.Exts (build)
	-- base

	module PrevLayout (prevLayout) where

	import XMonad
	import qualified XMonad.StackSet as W

	prevLayout :: X ()
	prevLayout = do
	[email protected]{ W.current = [email protected]{ W.workspace = ws }} <- gets windowset
	mp <- findPrev (description (W.layout ws)) (W.layout ws)
	case mp of

	{-# LANGUAGE RankNTypes, QuantifiedConstraints, BlockArguments, LambdaCase #-}

	module Free where

	-- base
	import Data.Coerce (coerce)


	type f ~> g = forall x. f x -> g x

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

	module Heap (
	Poset(..), Prefix(..),
	Heap, size,
	empty, singleton,
	insert, (<+>), fromList,
	pop, assocs,
	) where

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

	{-# LANGUAGE GHC2021, RoleAnnotations #-}

	module ID (
	ID, newID,
	sameID,
	) where

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

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