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
-- 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 |
{-# LANGUAGE RankNTypes, PolyKinds, GeneralisedNewtypeDeriving #-} | |
module EventManager ( | |
EventManager, | |
EventTag, eventTag, | |
attach, trigger, | |
) where | |
-- base | |
import Prelude hiding (lookup) |
{-# 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. |
-- 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(..), |
{-# 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) |
{-# LANGUAGE DataKinds, TypeFamilies, UndecidableInstances, RoleAnnotations | |
, QuantifiedConstraints, RebindableSyntax, BlockArguments | |
, RequiredTypeArguments | |
#-} | |
module Graded ( | |
GradedAppl(..), (<*>), (<*), (*>), | |
GradedAlt(..), | |
GradedMonad(..), (>>), |
{-# 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) |
{-# LANGUAGE QuantifiedConstraints | |
, UndecidableInstances | |
, AllowAmbiguousTypes | |
#-} | |
{-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-} | |
module LeibnizC where | |
import Leibniz |