Rewrite and generalize most of the library; partial LinearTypes support.
I had to move back to explicit arguments rather than associated types as my representation of categories because a functor may be a functor in multiple categories (e.g. ((,) a) is a functor in both the category of linear and intuitionistic implication). This also allowed me to get rid of some bad boilerplate involving `(:~:)` and some related issues. I also finally managed to get Monads as monoids in the category of endofunctors again. I don't recall what prevented me from doing it in the last iteration, but I think it's probably working now. It could just be that I understand the theory better and it's easier for me to get right now. There's still some unimplemented stuff that I'd like, pretty bad usability issues that I'd like to work around, and a dire lack of documentation. I intend to work on all that soon. The stack stuff has been removed because stackage doesn't have GHC 9 yet, and the template-haskell stuff has been removed until I can rewrite it, seeing as it was essentially useless as it was. The LinearTypes support is very incomplete, but it's supported in some places and I don't think I'd have much trouble expanding to support it in general; I just haven't had much time to experiment with it yet.master
parent
ae0795f0a3
commit
d90d3ad679
GPG Key ID:
4B7F3DA9351E577C
|
|
@ -11,9 +11,9 @@ jobs:
|
|||
uses: actions/checkout@v2
|
||||
|
||||
- name: Install latest Haskell Stack
|
||||
uses: actions/setup-haskell@v1.1
|
||||
uses: haskell/actions/setup@v1
|
||||
with:
|
||||
enable-stack: true
|
||||
ghc-version: '9.0.1'
|
||||
|
||||
- name: Build
|
||||
run: stack build
|
||||
run: cabal v2-build
|
||||
|
|
|
|||
|
|
@ -1,3 +1,10 @@
|
|||
# Stack working files
|
||||
.stack-work/
|
||||
stack.yaml.lock
|
||||
|
||||
# Cabal working files
|
||||
dist/
|
||||
dist-newstyle/
|
||||
|
||||
# Emacs backup files
|
||||
*~
|
||||
stack.yaml.lock
|
||||
|
|
@ -1,12 +1,15 @@
|
|||
# Monoids in the Category of Endofunctors
|
||||
This is a **toy** library for studying the field of [Abstract Nonsense](https://en.wikipedia.org/wiki/Abstract_nonsense) through Haskell.
|
||||
I would fire anyone who tried to do any of this crap in production.
|
||||
Writing this sort of code makes for a fun puzzle, but I want to be *absolutely clear*
|
||||
that I would *never* do anything even remotely close to this in a serious codebase.
|
||||
If you want to see code more representative of me as a programming practitioner,
|
||||
please refer to pretty much any project other than this one.
|
||||
|
||||
This library currently includes:
|
||||
* Category theory (`Category`)
|
||||
* Recursion schemes (`Category.Functor.Foldable`)
|
||||
* Dependent types, type-level programming, and codata (`Data`)
|
||||
* Dependent quantifiers (as a typeclass; `Quantifier`)
|
||||
* Dependent quantifiers (implemented with the help of a typeclass; `Quantifier`)
|
||||
|
||||
For further information, build and read the Haddock.
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,3 @@
|
|||
cradle:
|
||||
cabal:
|
||||
component: "lib:haskell-language-server"
|
||||
|
|
@ -1,11 +1,5 @@
|
|||
cabal-version: 2.2
|
||||
|
||||
-- This file has been generated from package.yaml by hpack version 0.33.0.
|
||||
--
|
||||
-- see: https://github.com/sol/hpack
|
||||
--
|
||||
-- hash: 09f2a99c2b84f61ffd46f9cbdb6958c3b1ac66bc38e80f8b92e02d5fa0813490
|
||||
|
||||
name: monoids-in-the-category-of-endofunctors
|
||||
version: 0.1.0.0
|
||||
description: Please see the README on GitHub at <https://github.com/jamestmartin/monoids-in-the-categoy-of-endofunctors#readme>
|
||||
|
|
@ -26,29 +20,79 @@ source-repository head
|
|||
|
||||
library
|
||||
exposed-modules:
|
||||
Category
|
||||
Category.Base
|
||||
Category.Constraint
|
||||
Category.Enriched
|
||||
Category.Functor
|
||||
Category.Functor.Foldable
|
||||
Category.Functor.Foldable.TH
|
||||
Category.Groupoid
|
||||
Category.Monoid
|
||||
Category.Monoidal
|
||||
Category.Unit
|
||||
Category.Void
|
||||
Category.Semigroup
|
||||
Data.Dict
|
||||
Data.Fin
|
||||
Data.Identity
|
||||
Data.Nat
|
||||
Data.Proxy
|
||||
Data.Vec
|
||||
Quantifier
|
||||
other-modules:
|
||||
Paths_monoids_in_the_category_of_endofunctors
|
||||
hs-source-dirs:
|
||||
src
|
||||
default-extensions: BlockArguments ConstraintKinds DataKinds DefaultSignatures EmptyCase FlexibleContexts FlexibleInstances FunctionalDependencies GADTs ImportQualifiedPost InstanceSigs LambdaCase MultiParamTypeClasses NoImplicitPrelude PatternSynonyms PolyKinds QuantifiedConstraints RankNTypes ScopedTypeVariables TypeApplications TypeFamilies TypeOperators ViewPatterns
|
||||
default-extensions:
|
||||
ApplicativeDo
|
||||
BangPatterns
|
||||
BinaryLiterals
|
||||
BlockArguments
|
||||
ConstraintKinds
|
||||
DataKinds
|
||||
DefaultSignatures
|
||||
DeriveDataTypeable
|
||||
DeriveFoldable
|
||||
DeriveFunctor
|
||||
DeriveGeneric
|
||||
DeriveLift
|
||||
DeriveTraversable
|
||||
DerivingStrategies
|
||||
EmptyCase
|
||||
EmptyDataDeriving
|
||||
ExistentialQuantification
|
||||
ExplicitForAll
|
||||
FlexibleContexts
|
||||
FlexibleInstances
|
||||
FunctionalDependencies
|
||||
GADTs
|
||||
GeneralizedNewtypeDeriving
|
||||
HexFloatLiterals
|
||||
ImportQualifiedPost
|
||||
InstanceSigs
|
||||
KindSignatures
|
||||
LambdaCase
|
||||
LinearTypes
|
||||
MultiParamTypeClasses
|
||||
MultiWayIf
|
||||
NamedFieldPuns
|
||||
NamedWildCards
|
||||
NoImplicitPrelude
|
||||
NumericUnderscores
|
||||
OverloadedStrings
|
||||
PartialTypeSignatures
|
||||
PatternSynonyms
|
||||
PolyKinds
|
||||
PostfixOperators
|
||||
QuantifiedConstraints
|
||||
RankNTypes
|
||||
ScopedTypeVariables
|
||||
StandaloneDeriving
|
||||
StandaloneKindSignatures
|
||||
TupleSections
|
||||
TypeApplications
|
||||
TypeFamilyDependencies
|
||||
TypeOperators
|
||||
TypeSynonymInstances
|
||||
ViewPatterns
|
||||
ghc-options: -Weverything -Wno-missing-export-lists -Wno-missing-import-lists -Wno-missing-safe-haskell-mode -Wno-safe -Wno-unsafe
|
||||
build-depends:
|
||||
base >=4.13 && <5
|
||||
, template-haskell >=2.16 && <3
|
||||
base >=4.14 && <5
|
||||
, ghc-prim >=0.7 && <0.8
|
||||
default-language: Haskell2010
|
||||
|
|
|
|||
53
package.yaml
53
package.yaml
|
|
@ -1,53 +0,0 @@
|
|||
name: monoids-in-the-category-of-endofunctors
|
||||
version: 0.1.0.0
|
||||
github: "jamestmartin/monoids-in-the-categoy-of-endofunctors"
|
||||
license: GPL-3.0-or-later
|
||||
author: "James Martin"
|
||||
maintainer: "james@jtmar.me"
|
||||
copyright: "Copyright: (C) 2020 James Martin"
|
||||
|
||||
extra-source-files:
|
||||
- README.md
|
||||
|
||||
description: Please see the README on GitHub at <https://github.com/jamestmartin/monoids-in-the-categoy-of-endofunctors#readme>
|
||||
|
||||
default-extensions:
|
||||
- BlockArguments
|
||||
- ConstraintKinds
|
||||
- DataKinds
|
||||
- DefaultSignatures
|
||||
- EmptyCase
|
||||
- FlexibleContexts
|
||||
- FlexibleInstances
|
||||
- FunctionalDependencies
|
||||
- GADTs
|
||||
- ImportQualifiedPost
|
||||
- InstanceSigs
|
||||
- LambdaCase
|
||||
- MultiParamTypeClasses
|
||||
- NoImplicitPrelude
|
||||
- PatternSynonyms
|
||||
- PolyKinds
|
||||
- QuantifiedConstraints
|
||||
- RankNTypes
|
||||
- ScopedTypeVariables
|
||||
- TypeApplications
|
||||
- TypeFamilies
|
||||
- TypeOperators
|
||||
- ViewPatterns
|
||||
|
||||
ghc-options:
|
||||
- -Weverything
|
||||
#- -Werror
|
||||
- -Wno-missing-export-lists
|
||||
- -Wno-missing-import-lists
|
||||
- -Wno-missing-safe-haskell-mode
|
||||
- -Wno-safe
|
||||
- -Wno-unsafe
|
||||
|
||||
dependencies:
|
||||
- base >= 4.13 && < 5
|
||||
- template-haskell >= 2.16 && < 3
|
||||
|
||||
library:
|
||||
source-dirs: src
|
||||
|
|
@ -1,15 +0,0 @@
|
|||
-- | A category theory prelude which re-exports other modules.
|
||||
-- Please refer to their respective haddocks.
|
||||
--
|
||||
-- This does not export *every* category module;
|
||||
-- only those which are likely to be relevant to every program.
|
||||
-- For example, "Category.Functor.Foldable" is not included here.
|
||||
module Category
|
||||
( module Category.Base
|
||||
, module Category.Constraint
|
||||
, module Category.Functor
|
||||
) where
|
||||
|
||||
import Category.Base
|
||||
import Category.Constraint
|
||||
import Category.Functor
|
||||
|
|
@ -1,58 +1,42 @@
|
|||
module Category.Base where
|
||||
|
||||
import Data.Dict (Dict (Dict))
|
||||
import Data.Kind (Constraint, Type)
|
||||
import Data.Dict
|
||||
import Data.Kind (Constraint, FUN, Type)
|
||||
import GHC.Types (Multiplicity)
|
||||
|
||||
-- | A typeclass which is implemented for everything.
|
||||
class Vacuous (a :: i)
|
||||
instance Vacuous (a :: i)
|
||||
-- | A one-parameter typeclass which is always implemented.
|
||||
type Unconst1 :: i -> Constraint
|
||||
class Unconst1 a
|
||||
instance Unconst1 a
|
||||
|
||||
class Semigroupoid (q :: i -> i -> Type) where
|
||||
type Obj q :: i -> Constraint
|
||||
type Obj _ = Vacuous
|
||||
observe :: a `q` b -> Dict (Obj q a, Obj q b)
|
||||
default observe :: Obj q ~ Vacuous => a `q` b -> Dict (Obj q a, Obj q b)
|
||||
observe _ = Dict
|
||||
type Category :: forall i. (i -> i -> Type) -> Constraint
|
||||
-- Scoped type variables does not make `i` in scope with standalone kind signatures,
|
||||
-- so this redundant type annotation is necessary.
|
||||
class Category (morph :: i -> i -> Type) where
|
||||
type Obj morph :: i -> Constraint
|
||||
type Obj _morph = Unconst1
|
||||
obj :: morph a b -> Dict (Obj morph a, Obj morph b)
|
||||
default obj :: forall a b. Obj morph ~ Unconst1 => morph a b -> Dict (Obj morph a, Obj morph b)
|
||||
obj _ = Dict
|
||||
|
||||
id :: Obj morph a => morph a a
|
||||
-- | Associative composition of morphisms.
|
||||
(.) :: b `q` c -> a `q` b -> a `q` c
|
||||
(.) :: morph b c -> morph a b -> morph a c
|
||||
|
||||
instance Semigroupoid (->) where
|
||||
(.) f g x = f (g x)
|
||||
instance forall (m :: Multiplicity). Category (FUN m) where
|
||||
id = \x -> x
|
||||
f . g = \x -> f (g x)
|
||||
|
||||
class Semigroupoid q => Category q where
|
||||
id :: Obj q a => a `q` a
|
||||
type Yoneda :: (i -> i -> Type) -> i -> i -> Type
|
||||
newtype Yoneda morph a b = Op { getOp :: morph b a }
|
||||
|
||||
instance Category (->) where
|
||||
id x = x
|
||||
|
||||
class Category q => Groupoid q where
|
||||
inv :: a `q` b -> b `q` a
|
||||
|
||||
newtype Yoneda (q :: i -> i -> Type) (a :: i) (b :: i) = Op { getOp :: b `q` a }
|
||||
|
||||
instance Semigroupoid q => Semigroupoid (Yoneda q) where
|
||||
type Obj (Yoneda q) = Obj q
|
||||
observe (Op f) = case observe f of Dict -> Dict
|
||||
instance Category morph => Category (Yoneda morph) where
|
||||
type Obj (Yoneda morph) = Obj morph
|
||||
obj (Op f) = case obj f of Dict -> Dict
|
||||
id = Op id
|
||||
Op f . Op g = Op (g . f)
|
||||
|
||||
instance Category q => Category (Yoneda q) where
|
||||
id = Op id
|
||||
|
||||
type family Op (q :: i -> i -> Type) :: i -> i -> Type where
|
||||
Op (Yoneda q) = q
|
||||
Op q = Yoneda q
|
||||
|
||||
type Post f = forall a. f a
|
||||
type Endo f a = f a a
|
||||
|
||||
data (:~:) :: i -> i -> Type where
|
||||
Refl :: a :~: a
|
||||
|
||||
instance Semigroupoid (:~:) where
|
||||
Refl . Refl = Refl
|
||||
|
||||
instance Category (:~:) where
|
||||
id = Refl
|
||||
|
||||
instance Groupoid (:~:) where
|
||||
inv Refl = Refl
|
||||
type Op :: (i -> i -> Type) -> i -> i -> Type
|
||||
type family Op morph where
|
||||
Op (Yoneda morph) = morph
|
||||
Op morph = Yoneda morph
|
||||
|
|
|
|||
|
|
@ -1,19 +1,51 @@
|
|||
module Category.Constraint
|
||||
( module Data.Dict
|
||||
, (:-) (Sub)
|
||||
, (\\)
|
||||
) where
|
||||
{-# LANGUAGE UndecidableSuperClasses #-}
|
||||
module Category.Constraint where
|
||||
|
||||
import Category.Base
|
||||
import Category.Functor
|
||||
import Category.Monoidal
|
||||
import Data.Dict
|
||||
import Data.Kind (Constraint, Type)
|
||||
|
||||
newtype a :- b = Sub (a => Dict b)
|
||||
type (:-) :: Constraint -> Constraint -> Type
|
||||
data (:-) c d = Sub (c => Dict d)
|
||||
|
||||
(\\) :: a => (b => c) -> (a :- b) -> c
|
||||
r \\ Sub Dict = r
|
||||
|
||||
instance Semigroupoid (:-) where
|
||||
f . g = Sub (Dict \\ f \\ g)
|
||||
|
||||
instance Category (:-) where
|
||||
id = Sub Dict
|
||||
f . g = Sub (Dict \\ f \\ g)
|
||||
|
||||
instance Functor (Nat (->) (:-)) (Yoneda (:-)) (:-) where
|
||||
map_ _ _ = Dict
|
||||
map (Op (Sub f)) = Nat \(Sub g) -> Sub case f of Dict -> case g of Dict -> Dict
|
||||
|
||||
instance Functor (->) (:-) ((:-) a) where
|
||||
map = (.)
|
||||
|
||||
instance Functor (->) (:-) Dict where
|
||||
map f = \Dict -> case f of Sub Dict -> Dict
|
||||
|
||||
class (c, d) => ProdC c d
|
||||
instance (c, d) => ProdC c d
|
||||
-- Note that, to my understanding,
|
||||
-- it is impossible to define disjunction in the category of constraints,
|
||||
-- and as far as I know this is the only way in which entailment is monoidal
|
||||
-- (up to isomorphism), although I haven't seriously thought about it at all.
|
||||
|
||||
instance Functor (Nat (:-) (:-)) (:-) ProdC where
|
||||
map_ _ _ = Dict
|
||||
map (Sub f) = Nat (Sub case f of Dict -> Dict)
|
||||
|
||||
instance Functor (:-) (:-) (ProdC a) where
|
||||
map (Sub f) = Sub case f of Dict -> Dict
|
||||
|
||||
instance Monoidal (:-) ProdC where
|
||||
type Unit (:-) ProdC = ()
|
||||
uil = Sub Dict
|
||||
uir = Sub Dict
|
||||
uel = Sub Dict
|
||||
uer = Sub Dict
|
||||
pal = Sub Dict
|
||||
par = Sub Dict
|
||||
|
|
|
|||
|
|
@ -0,0 +1,27 @@
|
|||
module Category.Enriched where
|
||||
|
||||
import Category.Base
|
||||
import Category.Monoidal
|
||||
import Data.Dict
|
||||
import Data.Kind (Constraint, FUN, Type)
|
||||
import GHC.Types (Multiplicity (One))
|
||||
|
||||
class Monoidal over prod => Enriched (over :: j -> j -> Type) prod (morph :: i -> i -> j) where
|
||||
type EObj over prod morph :: i -> Constraint
|
||||
type EObj _over _prod _morph = Unconst1
|
||||
eobj :: proxy prod -> over (Unit over prod) (morph a b) -> Dict (EObj over prod morph a, EObj over prod morph b)
|
||||
default eobj :: forall proxy a b. EObj over prod morph ~ Unconst1 => proxy prod -> over (Unit over prod) (morph a b) -> Dict (EObj over prod morph a, EObj over prod morph b)
|
||||
eobj _ _ = Dict
|
||||
|
||||
eid :: EObj over prod morph a => proxy prod -> over (Unit over prod) (morph a a)
|
||||
ecomp :: over (prod (morph b c) (morph a b)) (morph a c)
|
||||
|
||||
instance Category morph => Enriched (->) (,) morph where
|
||||
type EObj (->) (,) morph = Obj morph
|
||||
eobj _ f = obj (f ())
|
||||
eid _ = \() -> id
|
||||
ecomp = \(f, g) -> f . g
|
||||
|
||||
instance Enriched (FUN 'One) (,) (FUN 'One) where
|
||||
eid _ = \() -> id
|
||||
ecomp = \(f, g) -> \x -> f (g x)
|
||||
|
|
@ -2,136 +2,106 @@
|
|||
module Category.Functor where
|
||||
|
||||
import Category.Base
|
||||
import Category.Constraint ((:-) (Sub), Dict (Dict))
|
||||
import Data.Dict
|
||||
import Data.Either (Either (Left, Right))
|
||||
import Data.Kind (Type)
|
||||
import Data.Kind (Constraint, FUN, Type)
|
||||
import Data.Maybe (Maybe (Nothing, Just))
|
||||
import Quantifier
|
||||
import Data.Proxy
|
||||
|
||||
class (Category (Dom f), Category (Cod f)) => Functor (f :: i -> j) where
|
||||
type Dom f :: i -> i -> Type
|
||||
type Cod f :: j -> j -> Type
|
||||
map_ :: Obj (Dom f) a :- Obj (Cod f) (f a)
|
||||
default map_ :: Obj (Cod f) ~ Vacuous => Obj (Dom f) a :- Obj (Cod f) (f a)
|
||||
map_ = Sub Dict
|
||||
map :: Dom f a b -> Cod f (f a) (f b)
|
||||
type Functor :: (j -> j -> Type) -> (i -> i -> Type) -> (i -> j) -> Constraint
|
||||
class (Category dest, Category src) => Functor dest src f where
|
||||
map_ :: Obj src a => proxy dest -> proxy' src -> Dict (Obj dest (f a))
|
||||
default map_ :: forall proxy proxy' a. Obj dest ~ Unconst1 => proxy dest -> proxy' src -> Dict (Obj dest (f a))
|
||||
map_ _ _ = Dict
|
||||
map :: src a b -> dest (f a) (f b)
|
||||
|
||||
class (Functor f, Dom f ~ q, Cod f ~ r) => FunctorOf q r f
|
||||
instance (Functor f, Dom f ~ q, Cod f ~ r) => FunctorOf q r f
|
||||
type Endo f a = f a a
|
||||
type Endofunctor :: (i -> i -> Type) -> (i -> i) -> Constraint
|
||||
class Endo Functor morph f => Endofunctor morph f where
|
||||
instance Endo Functor morph f => Endofunctor morph f
|
||||
endomap :: Endofunctor morph f => morph a b -> morph (f a) (f b)
|
||||
endomap = map
|
||||
|
||||
class (Functor f, Dom f ~ Cod f) => Endofunctor f
|
||||
instance (Functor f, Dom f ~ Cod f) => Endofunctor f
|
||||
class Contravariant dest src f where
|
||||
contramap :: src b a -> dest (f a) (f b)
|
||||
|
||||
data Nat (q :: i -> i -> Type) (r :: j -> j -> Type) (f :: i -> j) (g :: i -> j) :: Type where
|
||||
Nat :: (FunctorOf q r f, FunctorOf q r g) => { runNat :: forall a. Obj q a => r (f a) (g a) } -> Nat q r f g
|
||||
instance {-# INCOHERENT #-} Functor dest (Yoneda src) f => Contravariant dest src f where
|
||||
contramap f = map (Op f)
|
||||
|
||||
instance Semigroupoid r => Semigroupoid (Nat q r) where
|
||||
type Obj (Nat q r) = FunctorOf q r
|
||||
observe (Nat _) = Dict
|
||||
(.) (Nat f) (Nat g) = Nat (f . g)
|
||||
instance {-# INCOHERENT #-} Functor dest src f => Contravariant dest (Yoneda src) f where
|
||||
contramap (Op f) = map f
|
||||
|
||||
instance Category r => Category (Nat q r) where
|
||||
id :: forall f. Obj (Nat q r) f => Nat q r f f
|
||||
-- FIXME:
|
||||
-- I'm not convinced this definition is sufficient.
|
||||
-- Don't feel like explaining why. Hopefully it won't be too long before I fix it.
|
||||
-- I'd hate to forget~
|
||||
type Bifunctor :: (j -> j -> Type) -> (i -> i -> Type) -> (i -> i -> j) -> Constraint
|
||||
class (Functor (Nat dest src) src f, forall x. Functor dest src (f x)) => Bifunctor dest src f
|
||||
instance (Functor (Nat dest src) src f, forall x. Functor dest src (f x)) => Bifunctor dest src f
|
||||
bimap :: forall dest src f a b c d. Bifunctor dest src f => src a c -> src b d -> dest (f a b) (f c d)
|
||||
bimap f g = case obj g of Dict -> runNat @_ @_ @dest @src (map f) . map g
|
||||
--first :: forall dest src f a b c d. Bifunctor dest src f => src a b -> dest (f a c) (f b c)
|
||||
--first f = runNat @_ @_ @dest @src (map f)
|
||||
second :: Bifunctor dest src f => src b c -> dest (f a b) (f a c)
|
||||
second g = map g
|
||||
|
||||
type Profunctor :: (j -> j -> Type) -> (i -> i -> Type) -> (i -> i -> j) -> Constraint
|
||||
class (Functor (Nat dest src) (Yoneda src) f, forall x. Functor dest src (f x)) => Profunctor dest src f
|
||||
instance (Functor (Nat dest src) (Yoneda src) f, forall x. Functor dest src (f x)) => Profunctor dest src f
|
||||
dimap :: forall dest src f a b c d. Profunctor dest src f => src a b -> src c d -> dest (f b c) (f a d)
|
||||
dimap f g = case obj g of Dict -> runNat @_ @_ @dest @src (map (Op f)) . map g
|
||||
|
||||
type Nat :: (j -> j -> Type) -> (i -> i -> Type) -> (i -> j) -> (i -> j) -> Type
|
||||
data Nat dest src f g = (Functor dest src f, Functor dest src g) => Nat { runNat :: !(forall a. Obj src a => dest (f a) (g a)) }
|
||||
|
||||
instance Category dest => Category (Nat dest src) where
|
||||
type Obj (Nat dest src) = Functor dest src
|
||||
obj (Nat _) = Dict
|
||||
id :: forall f. Obj (Nat dest src) f => Nat dest src f f
|
||||
id = Nat id'
|
||||
where id' :: forall a. Obj q a => r (f a) (f a)
|
||||
id' = case map_ :: Obj q a :- Obj r (f a) of Sub Dict -> id
|
||||
where id' :: forall a. Obj src a => dest (f a) (f a)
|
||||
id' = case map_ (Proxy @dest) (Proxy @src) :: Dict (Obj dest (f a)) of Dict -> id
|
||||
Nat f . Nat g = Nat (f . g)
|
||||
|
||||
instance Functor (->) where
|
||||
type Dom (->) = Op (->)
|
||||
type Cod (->) = Nat (->) (->)
|
||||
map_ = Sub Dict
|
||||
map (Op f) = Nat (. f)
|
||||
instance Functor (->) (FUN m) (FUN m a) where
|
||||
map f = \g -> f . g
|
||||
|
||||
instance Functor ((->) a) where
|
||||
type Dom ((->) a) = (->)
|
||||
type Cod ((->) a) = (->)
|
||||
map f g = f . g
|
||||
instance Functor (Nat (->) (FUN m)) (Yoneda (FUN m)) (FUN m) where
|
||||
map_ _ _ = Dict
|
||||
map (Op f) = Nat \g -> g . f
|
||||
|
||||
instance Functor (:-) where
|
||||
type Dom (:-) = Op (:-)
|
||||
type Cod (:-) = Nat (:-) (->)
|
||||
map_ = Sub Dict
|
||||
map (Op f) = Nat (. f)
|
||||
|
||||
instance Functor ((:-) a) where
|
||||
type Dom ((:-) a) = (:-)
|
||||
type Cod ((:-) a) = (->)
|
||||
map = (.)
|
||||
|
||||
instance Functor (:~:) where
|
||||
type Dom (:~:) = (:~:)
|
||||
type Cod (:~:) = Nat (:~:) (->)
|
||||
map_ = Sub Dict
|
||||
map Refl = Nat id
|
||||
|
||||
instance Functor ((:~:) a) where
|
||||
type Dom ((:~:) a) = (:~:)
|
||||
type Cod ((:~:) a) = (->)
|
||||
map = (.)
|
||||
|
||||
instance Functor (,) where
|
||||
type Dom (,) = (->)
|
||||
type Cod (,) = Nat (->) (->)
|
||||
map_ = Sub Dict
|
||||
instance Functor (Nat (FUN m) (FUN m)) (FUN m) (,) where
|
||||
map_ _ _ = Dict
|
||||
map f = Nat \(x, y) -> (f x, y)
|
||||
|
||||
instance Functor ((,) a) where
|
||||
type Dom ((,) a) = (->)
|
||||
type Cod ((,) a) = (->)
|
||||
map f (x, y) = (x, f y)
|
||||
instance Functor (FUN m) (FUN m) ((,) a) where
|
||||
map f = \(x, y) -> (x, f y)
|
||||
|
||||
instance Functor Either where
|
||||
type Dom Either = (->)
|
||||
type Cod Either = Nat (->) (->)
|
||||
map_ = Sub Dict
|
||||
instance Functor (Nat (FUN m) (FUN m)) (FUN m) Either where
|
||||
map_ _ _ = Dict
|
||||
map f = Nat \case
|
||||
Left x -> Left (f x)
|
||||
Right y -> Right y
|
||||
Left y -> Left (f y)
|
||||
Right x -> Right x
|
||||
|
||||
instance Functor (Either a) where
|
||||
type Dom (Either a) = (->)
|
||||
type Cod (Either a) = (->)
|
||||
map _ (Left x) = Left x
|
||||
map f (Right y) = Right (f y)
|
||||
instance Functor (FUN m) (FUN m) (Either a) where
|
||||
map f = \case
|
||||
Left y -> Left y
|
||||
Right x -> Right (f x)
|
||||
|
||||
instance Functor Dict where
|
||||
type Dom Dict = (:-)
|
||||
type Cod Dict = (->)
|
||||
map f Dict = case f of Sub Dict -> Dict
|
||||
instance Functor (FUN m) (FUN m) Maybe where
|
||||
map f = \case
|
||||
Nothing -> Nothing
|
||||
Just x -> Just (f x)
|
||||
|
||||
type family NatDom (f :: (i -> j) -> (i -> j) -> Type) :: (i -> i -> Type) where
|
||||
NatDom (Nat p _) = p
|
||||
instance {-# INCOHERENT #-} Category src => Functor (FUN m) src Proxy where
|
||||
map _ = \Proxy -> Proxy
|
||||
|
||||
type family NatCod (f :: (i -> j) -> (i -> j) -> Type) :: (j -> j -> Type) where
|
||||
NatCod (Nat _ q) = q
|
||||
type Const :: Type -> i -> Type
|
||||
newtype Const a b = Const { getConst :: a }
|
||||
|
||||
type Dom2 p = NatDom (Cod p)
|
||||
type Cod2 p = NatCod (Cod p)
|
||||
instance Functor (Nat (->) (->)) (->) Const where
|
||||
map_ _ _ = Dict
|
||||
map f = Nat \(Const x) -> Const (f x)
|
||||
|
||||
class (Functor p, Cod p ~ Nat (Dom2 p) (Cod2 p), Category (Dom2 p), Category (Cod2 p)) => Bifunctor (p :: i -> j -> k)
|
||||
instance (Functor p, Cod p ~ Nat (Dom2 p) (Cod2 p), Category (Dom2 p), Category (Cod2 p)) => Bifunctor (p :: i -> j -> k)
|
||||
|
||||
newtype Const (cat :: i -> i -> Type) (a :: Type) (b :: i) = Const { getConst :: a }
|
||||
|
||||
instance Category cat => Functor (Const cat a) where
|
||||
-- FIXME
|
||||
type Dom (Const cat a) = cat
|
||||
type Cod (Const cat a) = (->)
|
||||
map _ (Const x) = Const x
|
||||
|
||||
instance Category cat => Functor (Const cat) where
|
||||
type Dom (Const cat) = (->)
|
||||
type Cod (Const cat) = Nat cat (->)
|
||||
map_ = Sub Dict
|
||||
map f = Nat \case (Const x) -> Const (f x)
|
||||
|
||||
instance Functor Maybe where
|
||||
type Dom Maybe = (->)
|
||||
type Cod Maybe = (->)
|
||||
map _ Nothing = Nothing
|
||||
map f (Just x) = Just (f x)
|
||||
|
||||
instance {-# OVERLAPPABLE #-} Pi ty => Functor (Ty ty) where
|
||||
type Dom (Ty ty) = (:~:)
|
||||
type Cod (Ty ty) = (->)
|
||||
map Refl x = x
|
||||
instance {-# INCOHERENT #-} Category src => Functor (->) src (Const a) where
|
||||
map _ = \(Const x) -> Const x
|
||||
|
|
|
|||
|
|
@ -5,18 +5,18 @@ import Category.Functor
|
|||
|
||||
type family Base (t :: i) :: i -> i
|
||||
|
||||
class Endofunctor (Base t) => Recursive t where
|
||||
project :: Dom (Base t) t (Base t t)
|
||||
class Endofunctor morph (Base t) => Recursive morph t where
|
||||
project :: morph t (Base t t)
|
||||
|
||||
class Endofunctor (Base t) => Corecursive t where
|
||||
embed :: Dom (Base t) (Base t t) t
|
||||
class Endofunctor morph (Base t) => Corecursive morph t where
|
||||
embed :: morph (Base t t) t
|
||||
|
||||
type Algebra f a = Dom f (f a) a
|
||||
type Algebra morph f a = morph (f a) a
|
||||
|
||||
cata :: Recursive t => Algebra (Base t) a -> Dom (Base t) t a
|
||||
cata :: Recursive morph t => Algebra morph (Base t) a -> morph t a
|
||||
cata alg = alg . map (cata alg) . project
|
||||
|
||||
type Coalgebra f a = Dom f a (f a)
|
||||
type Coalgebra morph f a = morph a (f a)
|
||||
|
||||
ana :: Corecursive t => Coalgebra (Base t) a -> Dom (Base t) a t
|
||||
ana :: Corecursive morph t => Coalgebra morph (Base t) a -> morph a t
|
||||
ana coalg = embed . map (ana coalg) . coalg
|
||||
|
|
|
|||
|
|
@ -1,118 +0,0 @@
|
|||
-- | This module is incomplete and buggy! Do not use it!
|
||||
module Category.Functor.Foldable.TH where
|
||||
|
||||
--
|
||||
-- This code was my first time writing template Haskell.
|
||||
-- It was shoddily thrown together and is in severe need of a rewrite.
|
||||
--
|
||||
|
||||
import Data.Char (GeneralCategory (..), generalCategory)
|
||||
import Data.Maybe (fromMaybe, isNothing)
|
||||
import Language.Haskell.TH
|
||||
import Language.Haskell.TH.Syntax
|
||||
import Prelude
|
||||
|
||||
-- Copied from recursion-schemes
|
||||
isPuncChar :: Char -> Bool
|
||||
isPuncChar c = c `elem` ",;()[]{}`"
|
||||
|
||||
isSymbolChar :: Char -> Bool
|
||||
isSymbolChar c = not (isPuncChar c) && case generalCategory c of
|
||||
MathSymbol -> True
|
||||
CurrencySymbol -> True
|
||||
ModifierSymbol -> True
|
||||
OtherSymbol -> True
|
||||
DashPunctuation -> True
|
||||
OtherPunctuation -> c `notElem` "'\""
|
||||
ConnectorPunctuation -> c /= '_'
|
||||
_ -> False
|
||||
|
||||
fName :: Name -> Name
|
||||
fName orig = mkName (f (nameBase orig))
|
||||
where f name | isInfixName name = name ++ "$"
|
||||
| otherwise = name ++ "F"
|
||||
|
||||
isInfixName :: String -> Bool
|
||||
isInfixName = all isSymbolChar
|
||||
|
||||
unBndr :: TyVarBndr -> Kind
|
||||
unBndr (KindedTV _ k) = k
|
||||
unBndr _ = error "Automatically generated variable binders should have kind annotations."
|
||||
|
||||
-- | For a type `MyType (a :: i) (b :: j) :: k -> l -> Type`,
|
||||
-- create a base functor `MyTypeF (a :: i) (b :: j) (r :: k -> l -> Type) :: k -> l -> Type`
|
||||
-- such that `Fix (MyTypeF a b) c d` is isomorphic to `MyType a b c d`.
|
||||
makeBaseFunctor :: Name -> Int -> DecsQ
|
||||
makeBaseFunctor refName pos = do
|
||||
-- The name for the variable for instances of recursion.
|
||||
recName <- newName "r"
|
||||
TyConI (DataD ctx origName varBndrs kind' origCons _) <- reify refName
|
||||
let newN = fName origName
|
||||
let actualVars = take pos varBndrs
|
||||
let kind = if pos == length varBndrs && isNothing kind'
|
||||
then Nothing
|
||||
else Just (foldr (\ty tys -> AppT (AppT ArrowT (unBndr ty)) tys) (fromMaybe StarT kind') (drop pos varBndrs))
|
||||
-- The kind of the recursive variable should be the same as the kind of the original data type.
|
||||
-- Similarly, the kind of the new datatype is the same as the kind of the old.
|
||||
let recBndr = maybe (KindedTV recName StarT) (KindedTV recName) kind
|
||||
pure [DataD ctx newN (actualVars ++ [recBndr]) kind (map (ForallC [recBndr] [] . makeBaseConstructor (length varBndrs - pos) origName recName (concatMap conn origCons)) origCons) []]
|
||||
where
|
||||
conn :: Con -> [Name]
|
||||
conn (NormalC n _) = [n]
|
||||
conn (RecC n _) = [n]
|
||||
conn (InfixC _ n _) = [n]
|
||||
conn (ForallC _ _ con) = conn con
|
||||
conn (GadtC ns _ _) = ns
|
||||
conn (RecGadtC ns _ _) = ns
|
||||
|
||||
makeBaseType :: Name -> Name -> [Name] -> Type -> Type
|
||||
makeBaseType orig recn conns = makeBaseType'
|
||||
where
|
||||
makeBaseType' (ForallT vars ctx ty) = ForallT vars (map makeBaseType' ctx) (makeBaseType' ty)
|
||||
makeBaseType' (ForallVisT vars ty) = ForallVisT vars (makeBaseType' ty)
|
||||
makeBaseType' (AppT t1 t2) = AppT (makeBaseType' t1) (makeBaseType' t2)
|
||||
makeBaseType' (AppKindT ty kn) = AppKindT (makeBaseType' ty) (makeBaseType' kn)
|
||||
makeBaseType' (SigT ty kn) = SigT (makeBaseType' ty) (makeBaseType' kn)
|
||||
makeBaseType' (VarT name) = VarT name
|
||||
makeBaseType' (ConT name)
|
||||
| name == orig = VarT recn
|
||||
| otherwise = ConT name
|
||||
makeBaseType' (PromotedT name)
|
||||
| name `elem` conns = PromotedT (fName name)
|
||||
| otherwise = PromotedT name
|
||||
makeBaseType' (InfixT ty1 name ty2) = InfixT (makeBaseType' ty1) name (makeBaseType' ty2)
|
||||
makeBaseType' (UInfixT ty1 name ty2) = UInfixT (makeBaseType' ty1) name (makeBaseType' ty2)
|
||||
makeBaseType' (ParensT ty) = ParensT (makeBaseType' ty)
|
||||
makeBaseType' o@(TupleT _) = o
|
||||
makeBaseType' o@(UnboxedTupleT _) = o
|
||||
makeBaseType' o@(UnboxedSumT _) = o
|
||||
makeBaseType' ArrowT = ArrowT
|
||||
makeBaseType' EqualityT = EqualityT
|
||||
makeBaseType' ListT = ListT
|
||||
makeBaseType' o@(PromotedTupleT _) = o
|
||||
makeBaseType' PromotedNilT = PromotedNilT
|
||||
makeBaseType' PromotedConsT = PromotedConsT
|
||||
makeBaseType' StarT = StarT
|
||||
makeBaseType' ConstraintT = ConstraintT
|
||||
makeBaseType' o@(LitT _) = o
|
||||
makeBaseType' WildCardT = WildCardT
|
||||
makeBaseType' (ImplicitParamT s ty) = ImplicitParamT s (makeBaseType' ty)
|
||||
|
||||
makeBaseBangType :: Name -> Name -> [Name] -> BangType -> BangType
|
||||
makeBaseBangType orig recn conns (bng, ty) = (bng, makeBaseType orig recn conns ty)
|
||||
|
||||
makeBaseVarBangType :: Name -> Name -> [Name] -> VarBangType -> VarBangType
|
||||
makeBaseVarBangType orig recn conns (var, bng, ty) = (fName var, bng, makeBaseType orig recn conns ty)
|
||||
|
||||
fixGadtTy :: Int -> Name -> Name -> [Name] -> Name -> Type -> Type
|
||||
fixGadtTy 0 orig recn conns name o = AppT (fixGadtTy (-1) orig recn conns name o) (VarT recn)
|
||||
fixGadtTy pos orig recn conns name (AppT a b) = AppT (fixGadtTy (pos - 1) orig recn conns name a) (makeBaseType orig recn conns b)
|
||||
fixGadtTy _ _ _ _ name _ = ConT (fName name)
|
||||
|
||||
makeBaseConstructor :: Int -> Name -> Name -> [Name] -> Con -> Con
|
||||
makeBaseConstructor pos orig recn conns (NormalC name tys) = NormalC (fName name) (map (makeBaseBangType orig recn conns) tys)
|
||||
makeBaseConstructor pos orig recn conns (RecC name tys) = RecC (fName name) (map (makeBaseVarBangType orig recn conns) tys)
|
||||
makeBaseConstructor pos orig recn conns (InfixC ty1 name ty2) = InfixC (makeBaseBangType orig recn conns ty1) (fName name) (makeBaseBangType orig recn conns ty2)
|
||||
makeBaseConstructor pos orig recn conns (ForallC vars ctx con) = ForallC vars (map (makeBaseType orig recn conns) ctx) (makeBaseConstructor pos orig recn conns con)
|
||||
makeBaseConstructor pos orig recn conns (GadtC names tys ty) = GadtC (map fName names) (map (makeBaseBangType orig recn conns) tys) (fixGadtTy pos orig recn conns orig ty)
|
||||
makeBaseConstructor pos orig recn conns (RecGadtC names tys ty) = RecGadtC (map fName names) (map (makeBaseVarBangType orig recn conns) tys) (fixGadtTy pos orig recn conns orig ty)
|
||||
|
|
@ -0,0 +1,8 @@
|
|||
module Category.Groupoid where
|
||||
|
||||
import Category.Base
|
||||
import Data.Kind (Constraint, Type)
|
||||
|
||||
type Groupoid :: (i -> i -> Type) -> Constraint
|
||||
class Category morph => Groupoid morph where
|
||||
inv :: morph a b -> morph b a
|
||||
|
|
@ -1,10 +1,22 @@
|
|||
module Category.Monoid where
|
||||
|
||||
import Category.Base
|
||||
import Category.Functor
|
||||
import Category.Monoidal
|
||||
import Category.Semigroup
|
||||
import Data.Dict
|
||||
import Data.Kind (Constraint, Type)
|
||||
import Data.Maybe (Maybe (Just))
|
||||
import Data.Proxy
|
||||
|
||||
class TensorProduct f => Semigroup (f :: i -> i -> i) (s :: i) where
|
||||
append :: Cod2 f (f s s) s
|
||||
type Monoid :: (i -> i -> Type) -> (i -> i -> i) -> i -> Constraint
|
||||
class Semigroup morph prod m => Monoid morph prod m where
|
||||
empty :: proxy morph -> proxy' prod -> morph (Unit morph prod) m
|
||||
|
||||
class Semigroup f m => Monoid f m where
|
||||
empty :: proxy f -> Cod2 f (Unit f) m
|
||||
instance Monoid (Nat (->) (->)) Compose Maybe where
|
||||
empty _ _ = Nat \(Identity x) -> Just x
|
||||
|
||||
(>>=) :: forall f a b. Monoid (Nat (->) (->)) Compose f => f a -> (a -> f b) -> f b
|
||||
m >>= f = runNat (append @_ @(Nat (->) (->))) m'
|
||||
where m' :: Compose f f b
|
||||
m' = case obj (empty @_ @_ @_ @f (Proxy @(Nat (->) (->))) (Proxy @Compose)) of Dict -> Compose (map f m)
|
||||
|
|
|
|||
|
|
@ -1,62 +1,83 @@
|
|||
-- | Monoidal categories.
|
||||
module Category.Monoidal where
|
||||
|
||||
import Category.Base
|
||||
import Category.Constraint
|
||||
import Category.Functor
|
||||
import Data.Dict
|
||||
import Data.Either (Either (Left, Right))
|
||||
import Data.Void (Void, absurd)
|
||||
import Data.Kind (Constraint, FUN, Type)
|
||||
import Data.Void (Void)
|
||||
|
||||
-- FIXME: Rename this.
|
||||
-- | A category is monoidal if it has a product and a unit for that product.
|
||||
-- A category can have multiple tensor products and be monoidal in multiple ways,
|
||||
-- including the category of types itself,
|
||||
-- so instead of using a @Monoidal@ typeclass, we use a @TensorProduct@ typeclass.
|
||||
class Bifunctor f => TensorProduct (f :: i -> i -> i) where
|
||||
-- | The identity object of the product.
|
||||
type Unit f :: i
|
||||
-- | The identity object is actually an object in the category.
|
||||
unitObj :: proxy f -> Dict (Obj (Dom f) (Unit f))
|
||||
-- Only we actually don't, because I haven't had a chance to rename it yet.
|
||||
type Monoidal :: (i -> i -> Type) -> (i -> i -> i) -> Constraint
|
||||
class Endo Bifunctor morph prod => Monoidal (morph :: i -> i -> Type) prod where
|
||||
-- FIXME: Fix all of these garbage names. `uil`? `pal`? seriously?
|
||||
type Unit morph prod :: i
|
||||
prodObj :: (Obj morph a, Obj morph b) => proxy morph -> proxy' prod -> proxy'' a -> proxy''' b -> Dict (Obj morph (prod a b))
|
||||
default prodObj :: Obj morph ~ Unconst1 => proxy morph -> proxy' prod -> proxy'' a -> proxy''' b -> Dict (Obj morph (prod a b))
|
||||
prodObj _ _ _ _ = Dict
|
||||
unitObj :: proxy morph -> proxy' prod -> Dict (Obj morph (Unit morph prod))
|
||||
default unitObj :: Obj morph ~ Unconst1 => proxy morph -> proxy' prod -> Dict (Obj morph (Unit morph prod))
|
||||
unitObj _ _ = Dict
|
||||
uil :: Obj morph a => morph a (prod (Unit morph prod) a)
|
||||
uir :: Obj morph a => morph a (prod a (Unit morph prod))
|
||||
uel :: Obj morph a => morph (prod (Unit morph prod) a) a
|
||||
uer :: Obj morph a => morph (prod a (Unit morph prod)) a
|
||||
pal :: (Obj morph a, Obj morph b, Obj morph c) => morph (prod a (prod b c)) (prod (prod a b) c)
|
||||
par :: (Obj morph a, Obj morph b, Obj morph c) => morph (prod (prod a b) c) (prod a (prod b c))
|
||||
|
||||
-- | 'Unit' is the identity of the product; introduce a value on the left of a product.
|
||||
unitLI :: Dom f a (f a (Unit f))
|
||||
-- | 'Unit' is the identity of the product; introduce a value on the right of a product.
|
||||
unitRI :: Dom f a (f (Unit f) a)
|
||||
-- | 'Unit' is the identity of the product; eliminate a product, projecting a value on the right.
|
||||
unitLE :: Dom f (f a (Unit f)) a
|
||||
-- | 'Unit' is the identity of the product; eliminate a product, projecting a value on the left.
|
||||
unitRE :: Dom f (f (Unit f) a) a
|
||||
instance Monoidal (FUN m) (,) where
|
||||
type Unit (FUN m) (,) = ()
|
||||
uil = \x -> ((), x)
|
||||
uir = \x -> (x, ())
|
||||
uel = \((), x) -> x
|
||||
uer = \(x, ()) -> x
|
||||
pal = \(x, (y, z)) -> ((x, y), z)
|
||||
par = \((x, y), z) -> (x, (y, z))
|
||||
|
||||
-- | The product is associative; associate to the left.
|
||||
assocL :: Dom f (f a (f b c)) (f (f a b) c)
|
||||
-- | The product is associative; associate to the right.
|
||||
assocR :: Dom f (f (f a b) c) (f a (f b c))
|
||||
instance Monoidal (FUN m) Either where
|
||||
type Unit (FUN m) Either = Void
|
||||
uil = Right
|
||||
uir = Left
|
||||
uel (Left x) = (\case{}) x
|
||||
uel (Right x) = x
|
||||
uer (Left x) = x
|
||||
uer (Right x) = (\case{}) x
|
||||
pal (Left x) = Left (Left x)
|
||||
pal (Right (Left x)) = Left (Right x)
|
||||
pal (Right (Right x)) = Right x
|
||||
par (Left (Left x)) = Left x
|
||||
par (Left (Right x)) = Right (Left x)
|
||||
par (Right x) = Right (Right x)
|
||||
|
||||
instance TensorProduct (,) where
|
||||
type Unit (,) = ()
|
||||
unitObj _ = Dict
|
||||
data Compose f g x = (Functor (->) (->) f, Functor (->) (->) g) => Compose { getCompose :: !(f (g x)) }
|
||||
newtype Identity x = Identity { getIdentity :: x }
|
||||
|
||||
unitLI x = (x, ())
|
||||
unitRI x = ((), x)
|
||||
unitLE (x, _) = x
|
||||
unitRE (_, x) = x
|
||||
instance Functor (FUN m) (FUN m) Identity where
|
||||
map f = \(Identity x) -> Identity (f x)
|
||||
|
||||
assocL (x, (y, z)) = ((x, y), z)
|
||||
assocR ((x, y), z) = (x, (y, z))
|
||||
instance Functor (->) (->) (Compose f g) where
|
||||
map f = \(Compose x) -> Compose (map @_ @_ @(->) @(->) (map f) x)
|
||||
|
||||
instance TensorProduct Either where
|
||||
type Unit Either = Void
|
||||
unitObj _ = Dict
|
||||
instance Functor (Nat (Nat (->) (->)) (Nat (->) (->))) (Nat (->) (->)) Compose where
|
||||
map_ _ _ = Dict
|
||||
map (Nat f) = Nat (Nat \(Compose x) -> Compose (f x))
|
||||
|
||||
unitLI = Left
|
||||
unitRI = Right
|
||||
unitLE (Left x) = x
|
||||
unitLE (Right x) = absurd x
|
||||
unitRE (Left x) = absurd x
|
||||
unitRE (Right x) = x
|
||||
instance Functor (Nat (->) (->)) (Nat (->) (->)) (Compose f) where
|
||||
map_ _ _ = Dict
|
||||
map (Nat f) = Nat \(Compose x) -> Compose (map f x)
|
||||
|
||||
assocL (Left x) = Left (Left x)
|
||||
assocL (Right (Left x)) = Left (Right x)
|
||||
assocL (Right (Right x)) = Right x
|
||||
assocR (Left (Left x)) = Left x
|
||||
assocR (Left (Right x)) = Right (Left x)
|
||||
assocR (Right x) = Right (Right x)
|
||||
instance Monoidal (Nat (->) (->)) Compose where
|
||||
type Unit (Nat (->) (->)) Compose = Identity
|
||||
prodObj _ _ _ _ = Dict
|
||||
unitObj _ _ = Dict
|
||||
uil = Nat \x -> Compose (Identity x)
|
||||
uir = Nat \x -> Compose (map Identity x)
|
||||
uel = Nat \(Compose (Identity x)) -> x
|
||||
uer = Nat \(Compose x) -> map getIdentity x
|
||||
pal = Nat \(Compose x) -> Compose (Compose (map getCompose x))
|
||||
par = Nat \(Compose (Compose x)) -> Compose (map Compose x)
|
||||
|
|
|
|||
|
|
@ -0,0 +1,18 @@
|
|||
module Category.Semigroup where
|
||||
|
||||
import Category.Functor
|
||||
import Category.Monoidal
|
||||
import Data.Kind (Constraint, Type)
|
||||
import Data.Maybe (Maybe (Nothing, Just))
|
||||
|
||||
type Semigroup :: (i -> i -> Type) -> (i -> i -> i) -> i -> Constraint
|
||||
class Monoidal morph prod => Semigroup morph prod s where
|
||||
append :: morph (prod s s) s
|
||||
|
||||
instance Semigroup (Nat (->) (->)) Compose Maybe where
|
||||
append = Nat \(Compose x') -> case x' of
|
||||
Nothing -> Nothing
|
||||
Just Nothing -> Nothing
|
||||
Just (Just x) -> Just x
|
||||
|
||||
-- TODO: More semigroup/monoid instances. `Either` has two, can I accomodate both?
|
||||
|
|
@ -1,16 +0,0 @@
|
|||
-- | The 'Unit' category contains exactly one object and one morphism.
|
||||
module Category.Unit where
|
||||
|
||||
import Category.Base
|
||||
|
||||
-- | A category with exactly one morphism.
|
||||
data Unit (a :: ()) (b :: ()) = Unit
|
||||
|
||||
instance Semigroupoid Unit where
|
||||
_ . _ = Unit
|
||||
|
||||
instance Category Unit where
|
||||
id = Unit
|
||||
|
||||
instance Groupoid Unit where
|
||||
inv _ = Unit
|
||||
|
|
@ -1,24 +0,0 @@
|
|||
-- | The `Void` category contains no objects and no morphisms.
|
||||
module Category.Void where
|
||||
|
||||
import Category.Base
|
||||
import Data.Proxy
|
||||
|
||||
-- | The type of no morphisms.
|
||||
data Void (a :: i) (b :: i)
|
||||
|
||||
-- | A typeclass which is not implemented for anything.
|
||||
-- It's possible to write an implementation for this because Haskell isn't total,
|
||||
-- but you really, really shouldn't.
|
||||
class Bottom (a :: i) where
|
||||
bottom :: forall b proxy. proxy a -> b
|
||||
|
||||
instance Semigroupoid Void where
|
||||
-- No values are objects.
|
||||
type Obj Void = Bottom
|
||||
observe = \case {}
|
||||
(.) = \case {}
|
||||
|
||||
instance Category Void where
|
||||
id :: forall a. Bottom a => Void a a
|
||||
id = bottom (Proxy @a)
|
||||
|
|
@ -1,7 +1,10 @@
|
|||
module Data.Dict where
|
||||
|
||||
import Data.Kind (Constraint, Type)
|
||||
|
||||
-- | Constraint instances can be stored as values with GADTs.
|
||||
data Dict c where
|
||||
type Dict :: Constraint -> Type
|
||||
data Dict c =
|
||||
-- | You can only use this type constructor if an instance of @c@ is in scope;
|
||||
-- pattern matching against it brings an instance of @c@ into scope.
|
||||
Dict :: c => Dict c
|
||||
c => Dict
|
||||
|
|
|
|||
|
|
@ -1,7 +1,9 @@
|
|||
module Data.Fin where
|
||||
|
||||
import Category
|
||||
import Category.Functor
|
||||
import Category.Functor.Foldable
|
||||
import Data.Dict
|
||||
import Data.Identity
|
||||
import Data.Kind (Type)
|
||||
import Data.Nat
|
||||
|
||||
|
|
@ -13,37 +15,25 @@ data FinF r :: N -> Type where
|
|||
FSF :: r n -> FinF r ('S n)
|
||||
type instance Base Fin = FinF
|
||||
|
||||
instance Functor Fin where
|
||||
type Dom Fin = (:~:)
|
||||
type Cod Fin = (->)
|
||||
map Refl x = x
|
||||
|
||||
instance Functor (FinF r) where
|
||||
type Dom (FinF r) = (:~:)
|
||||
type Cod (FinF r) = (->)
|
||||
map Refl x = x
|
||||
|
||||
instance Functor FinF where
|
||||
type Dom FinF = Nat (:~:) (->)
|
||||
type Cod FinF = Nat (:~:) (->)
|
||||
map_ = Sub Dict
|
||||
map :: forall f g. Nat (:~:) (->) f g -> Nat (:~:) (->) (FinF f) (FinF g)
|
||||
instance Functor (Nat (->) (:~:)) (Nat (->) (:~:)) FinF where
|
||||
map_ _ _ = Dict
|
||||
map :: forall f g. Nat (->) (:~:) f g -> Nat (->) (:~:) (FinF f) (FinF g)
|
||||
map (Nat f) = Nat \case
|
||||
FZF -> FZF
|
||||
(FSF r) -> FSF (f r)
|
||||
|
||||
instance Recursive Fin where
|
||||
instance Recursive (Nat (->) (:~:)) Fin where
|
||||
project = Nat \case
|
||||
FZ -> FZF
|
||||
(FS r) -> FSF r
|
||||
|
||||
instance Corecursive Fin where
|
||||
instance Corecursive (Nat (->) (:~:)) Fin where
|
||||
embed = Nat \case
|
||||
FZF -> FZ
|
||||
(FSF r) -> FS r
|
||||
|
||||
fin2nat :: Nat (:~:) (->) Fin (Const (:~:) N)
|
||||
fin2nat :: Nat (->) (:~:) Fin (Const N)
|
||||
fin2nat = cata (Nat alg)
|
||||
where alg :: FinF (Const (:~:) N) n -> Const (:~:) N n
|
||||
where alg :: FinF (Const N) n -> Const N n
|
||||
alg FZF = Const Z
|
||||
alg (FSF (Const n)) = Const (S n)
|
||||
|
|
|
|||
|
|
@ -0,0 +1,33 @@
|
|||
module Data.Identity where
|
||||
|
||||
import Category.Base
|
||||
import Category.Functor
|
||||
import Category.Groupoid
|
||||
import Data.Dict
|
||||
import Data.Kind (Type)
|
||||
|
||||
type (:~:) :: i -> i -> Type
|
||||
data (:~:) :: i -> i -> Type where
|
||||
Refl :: a :~: a
|
||||
|
||||
instance Category (:~:) where
|
||||
id = Refl
|
||||
Refl . Refl = Refl
|
||||
|
||||
instance Groupoid (:~:) where
|
||||
inv Refl = Refl
|
||||
|
||||
-- TODO: There are lots, lots more valid functor instances.
|
||||
instance {-# INCOHERENT #-} Functor (->) (:~:) f where
|
||||
map Refl = id
|
||||
|
||||
instance {-# INCOHERENT #-} Functor (->) (Yoneda (:~:)) f where
|
||||
map (Op Refl) = id
|
||||
|
||||
instance {-# INCOHERENT #-} Functor (Nat (->) (:~:)) (:~:) f where
|
||||
map_ _ _ = Dict
|
||||
map Refl = id
|
||||
|
||||
instance {-# INCOHERENT #-} Functor (Nat (->) (:~:)) (Yoneda (:~:)) f where
|
||||
map_ _ _ = Dict
|
||||
map (Op Refl) = id
|
||||
|
|
@ -1,8 +1,10 @@
|
|||
-- | The natural numbers and associated types and functions.
|
||||
module Data.Nat where
|
||||
|
||||
import Category
|
||||
import Category.Functor
|
||||
import Category.Functor.Foldable
|
||||
import Data.Dict
|
||||
import Data.Identity
|
||||
import Data.Kind (Type)
|
||||
import Data.Maybe (Maybe (Nothing, Just))
|
||||
import Quantifier
|
||||
|
|
@ -39,37 +41,30 @@ data NTyF r n where
|
|||
ZTyF :: NTyF r 'Z
|
||||
STyF :: r n -> NTyF r ('S n)
|
||||
|
||||
instance Functor (NTyF r) where
|
||||
type Dom (NTyF r) = (:~:)
|
||||
type Cod (NTyF r) = (->)
|
||||
map Refl x = x
|
||||
|
||||
instance Functor NTyF where
|
||||
type Dom NTyF = Nat (:~:) (->)
|
||||
type Cod NTyF = Nat (:~:) (->)
|
||||
map_ = Sub Dict
|
||||
instance Functor (Nat (->) (:~:)) (Nat (->) (:~:)) NTyF where
|
||||
map_ _ _ = Dict
|
||||
map (Nat f) = Nat \case
|
||||
ZTyF -> ZTyF
|
||||
(STyF r) -> STyF (f r)
|
||||
|
||||
type instance Base N = Maybe
|
||||
|
||||
instance Recursive N where
|
||||
instance Recursive (->) N where
|
||||
project Z = Nothing
|
||||
project (S n) = Just n
|
||||
|
||||
instance Corecursive N where
|
||||
instance Corecursive (->) N where
|
||||
embed Nothing = Z
|
||||
embed (Just n) = S n
|
||||
|
||||
type instance Base (Ty N) = NTyF
|
||||
|
||||
instance Recursive (Ty N) where
|
||||
instance Recursive (Nat (->) (:~:)) (Ty N) where
|
||||
project = Nat \case
|
||||
ZTy -> ZTyF
|
||||
(STy r) -> STyF r
|
||||
|
||||
instance Corecursive (Ty N) where
|
||||
instance Corecursive (Nat (->) (:~:)) (Ty N) where
|
||||
embed = Nat \case
|
||||
ZTyF -> ZTy
|
||||
(STyF r) -> STy r
|
||||
|
|
@ -80,9 +75,9 @@ type family (:+) (m :: N) (n :: N) :: N where
|
|||
'S m :+ n = 'S (m :+ n)
|
||||
|
||||
-- | A proof that the successor function is injective.
|
||||
injective :: forall m n. Ty N m -> ('S m ~ 'S n) :- (m ~ n)
|
||||
injective ZTy = Sub Dict
|
||||
injective (STy i) = case injective i of Sub Dict -> Sub Dict
|
||||
injective :: forall m n. Ty N m -> ('S m ~ 'S n) => Dict (m ~ n)
|
||||
injective ZTy = Dict
|
||||
injective (STy i) = case injective i of Dict -> Dict
|
||||
|
||||
-- | A proof that zero is the right identity of addition.
|
||||
-- (The constraint solver can prove the left identity on its own.)
|
||||
|
|
|
|||
|
|
@ -5,8 +5,11 @@
|
|||
-- 'Proxy' provides a better alternative for passing explicit type arguments.
|
||||
module Data.Proxy where
|
||||
|
||||
import Data.Kind (Type)
|
||||
|
||||
-- | A type family of singletons used for explicit type arguments without TypeApplications.
|
||||
data Proxy (a :: i) where
|
||||
type Proxy :: i -> Type
|
||||
data Proxy a where
|
||||
-- | You can specify the type used with @Proxy :: Proxy a@,
|
||||
-- or @Proxy \@a@ using TypeApplications.
|
||||
--
|
||||
|
|
|
|||
|
|
@ -1,62 +1,47 @@
|
|||
module Data.Vec where
|
||||
|
||||
import Category
|
||||
import Category.Base
|
||||
import Category.Functor
|
||||
import Category.Functor.Foldable
|
||||
import Data.Dict
|
||||
import Data.Fin
|
||||
import Data.Identity
|
||||
import Data.Kind (Type)
|
||||
import Data.Nat
|
||||
import Prelude (($))
|
||||
|
||||
type Vec :: Type -> N -> Type
|
||||
data Vec a :: N -> Type where
|
||||
VZ :: Vec a 'Z
|
||||
VS :: a -> Vec a n -> Vec a ('S n)
|
||||
type VecF :: Type -> (N -> Type) -> N -> Type
|
||||
data VecF a r :: N -> Type where
|
||||
VZF :: VecF a r 'Z
|
||||
VSF :: a -> r n -> VecF a r ('S n)
|
||||
type instance Base (Vec a) = (VecF a)
|
||||
type instance Base (Vec a) = VecF a
|
||||
|
||||
instance Functor (Vec a) where
|
||||
type Dom (Vec a) = (:~:)
|
||||
type Cod (Vec a) = (->)
|
||||
map Refl x = x
|
||||
|
||||
instance Functor Vec where
|
||||
type Dom Vec = (->)
|
||||
type Cod Vec = Nat (:~:) (->)
|
||||
map_ = Sub Dict
|
||||
instance Functor (Nat (->) (:~:)) (->) Vec where
|
||||
map_ _ _ = Dict
|
||||
map f = Nat \case
|
||||
VZ -> VZ
|
||||
(VS x r) -> VS (f x) (runNat (map f) r)
|
||||
(VS x r) -> VS (f x) (runNat (map @_ @_ @(Nat (->) (:~:)) f) r)
|
||||
|
||||
instance Functor (VecF a r) where
|
||||
type Dom (VecF a r) = (:~:)
|
||||
type Cod (VecF a r) = (->)
|
||||
map Refl x = x
|
||||
|
||||
instance Functor (VecF a) where
|
||||
type Dom (VecF a) = Nat (:~:) (->)
|
||||
type Cod (VecF a) = Nat (:~:) (->)
|
||||
map_ = Sub Dict
|
||||
instance Functor (Nat (->) (:~:)) (Nat (->) (:~:)) (VecF a) where
|
||||
map_ _ _ = Dict
|
||||
map (Nat f) = Nat \case
|
||||
VZF -> VZF
|
||||
(VSF x r) -> VSF x (f r)
|
||||
|
||||
instance Functor VecF where
|
||||
type Dom VecF = (->)
|
||||
type Cod VecF = Nat (Nat (:~:) (->)) (Nat (:~:) (->))
|
||||
map_ = Sub Dict
|
||||
instance Functor (Nat (Nat (->) (:~:)) (Nat (->) (:~:))) (->) VecF where
|
||||
map_ _ _ = Dict
|
||||
map f = Nat $ Nat \case
|
||||
VZF -> VZF
|
||||
(VSF x r) -> VSF (f x) r
|
||||
|
||||
type Ixr :: (N -> Type) -> Type -> N -> Type
|
||||
newtype Ixr ty r a = Ixr { getIxr :: ty a -> r }
|
||||
|
||||
instance Functor (Ixr ty r) where
|
||||
type Dom (Ixr ty r) = (:~:)
|
||||
type Cod (Ixr ty r) = (->)
|
||||
map Refl x = x
|
||||
|
||||
indexer :: Nat (:~:) (->) Fin (Ixr (Vec a) a)
|
||||
indexer :: Nat (->) (:~:) Fin (Ixr (Vec a) a)
|
||||
indexer = cata $ Nat \case
|
||||
FZF -> Ixr \case VS x _ -> x
|
||||
(FSF (Ixr r)) -> Ixr \case VS _ xs -> r xs
|
||||
|
|
|
|||
|
|
@ -28,6 +28,10 @@ module Quantifier where
|
|||
import Data.Kind (Constraint, Type)
|
||||
import Data.Maybe (Maybe (Nothing, Just))
|
||||
|
||||
-- | An explicit non-dependent universal quantifier.
|
||||
type Forall :: (a -> Type) -> Type
|
||||
newtype Forall f = Forall { runForall :: forall proxy x. proxy x -> f x }
|
||||
|
||||
-- | A typeclass faciliating explicit dependent quantifiers.
|
||||
class Pi (ty :: Type) where
|
||||
-- | The type family @`Ty` ty :: ty -> `Type`@ is isomorphic to @ty@,
|
||||
|
|
|
|||
|
|
@ -1,5 +0,0 @@
|
|||
# Required to use GHC 8.10, which is required for ImportQualifiedPost.
|
||||
resolver: nightly-2020-10-22
|
||||
|
||||
packages:
|
||||
- .
|
||||
Loading…
Reference in New Issue