statebox / idris-ct

formally verified category theory library

statebox

Statebox diagrams for Lamassu machines

idris-ct's Issues

define monoidal functors

https://en.wikipedia.org/wiki/Monoidal_functor

Doesn't build on Mac OSX 10.11.6

Using Elba. 27 libraries compiled successfully.

Then got error:

Couldn't build library target for statebox/idris-ct 0.1.0 (dir+/Users/murray/apps/idris-ct-master)

"idris" "--check" "-p" "contrib" "Idris/FunctorAsCFunctor.lidr"
./Idris/FunctorAsCFunctor.lidr:45:27-78:
|
45 | > functorPreserveId _ a = funExt (\x => functorIdentity {a} id (\v => Refl) x)
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking right hand side of functorPreserveId with expected type
functorOnMorphisms func a a (extIdentity a) = extIdentity (f a)

When checking an application of Idris.TypesAsCategoryExtensional.funExt:
Type mismatch between
map id x = id x (Type of functorIdentity x)
and
_ -> _ (Is functorIdentity x applied to too many arguments?)

    Specifically:
            Type mismatch between
                    (=) map id x
            and
                    \uv => _ -> uv

error: one or more packages couldn't be built

---

Any ideas?

Errors when building compare target

--->  Building idris-ct
Executing:  cd "/opt/local/var/macports/build/_opt_svacchanda_SonomaPorts_math_idris-ct/idris-ct/work/idris-ct-fbc7f633e0d86bfe5b56a2c4b9db6f780d59106d" && /usr/bin/make -j4 -w compare CC="/opt/local/var/macports/build/_opt_svacchanda_SonomaPorts_math_idris-ct/idris-ct/work/compwrap/cc/usr/bin/clang" CXX="/opt/local/var/macports/build/_opt_svacchanda_SonomaPorts_math_idris-ct/idris-ct/work/compwrap/cxx/usr/bin/clang++" OBJC="/opt/local/var/macports/build/_opt_svacchanda_SonomaPorts_math_idris-ct/idris-ct/work/compwrap/objc/usr/bin/clang" OBJCXX="/opt/local/var/macports/build/_opt_svacchanda_SonomaPorts_math_idris-ct/idris-ct/work/compwrap/objcxx/usr/bin/clang++" INSTALL="/usr/bin/install -c" 
make: Entering directory `/opt/local/var/macports/build/_opt_svacchanda_SonomaPorts_math_idris-ct/idris-ct/work/idris-ct-fbc7f633e0d86bfe5b56a2c4b9db6f780d59106d'
idris2 fileDiff/FileDiff.idr -o compare
Error: While processing right hand side of pathFromVect. When unifying:
    List ?elem
and:
    Vect ?len ?elem
Mismatch between: List ?elem and Vect ?len ?elem.

fileDiff.FileDiff:8:56--8:65
 4 | 
 5 | data FileSystem = DirTree String (List FileSystem) | FileTree String
 6 | 
 7 | pathFromVect : Vect n String -> String
 8 | pathFromVect xs = concat $ intersperse "/" $ reverse $ toList xs
                                                            ^^^^^^^^^

Error: While processing right hand side of linearize. Sorry, I can't find any elaboration which works. All errors:
If Data.Vect.reverse: When unifying:
    List String
and:
    Vect ?len ?elem
Mismatch between: List String and Vect ?len ?elem.

fileDiff.FileDiff:11:76--11:81
 07 | pathFromVect : Vect n String -> String
 08 | pathFromVect xs = concat $ intersperse "/" $ reverse $ toList xs
 09 | 
 10 | linearize : (depth : List String) -> FileSystem -> List String
 11 | linearize depth (DirTree n []) = [concat $ reverse $ intersperse "/" (n :: depth)]
                                                                                 ^^^^^

If Prelude.List.reverse: When unifying:
    Vect (?len + pred ?len) ?elem
and:
    List ?a
Mismatch between: Vect (?len + pred ?len) ?elem and List ?a.

fileDiff.FileDiff:11:54--11:82
 07 | pathFromVect : Vect n String -> String
 08 | pathFromVect xs = concat $ intersperse "/" $ reverse $ toList xs
 09 | 
 10 | linearize : (depth : List String) -> FileSystem -> List String
 11 | linearize depth (DirTree n []) = [concat $ reverse $ intersperse "/" (n :: depth)]
                                                           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

If Prelude.SnocList.reverse: When unifying:
    Vect (?len + pred ?len) ?elem
and:
    SnocList ?a
Mismatch between: Vect (?len + pred ?len) ?elem and SnocList ?a.

fileDiff.FileDiff:11:54--11:82
 07 | pathFromVect : Vect n String -> String
 08 | pathFromVect xs = concat $ intersperse "/" $ reverse $ toList xs
 09 | 
 10 | linearize : (depth : List String) -> FileSystem -> List String
 11 | linearize depth (DirTree n []) = [concat $ reverse $ intersperse "/" (n :: depth)]
                                                           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

If Prelude.reverse: When unifying:
    Vect (?len + pred ?len) ?elem
and:
    String
Mismatch between: Vect (?len + pred ?len) ?elem and String.

fileDiff.FileDiff:11:54--11:82
 07 | pathFromVect : Vect n String -> String
 08 | pathFromVect xs = concat $ intersperse "/" $ reverse $ toList xs
 09 | 
 10 | linearize : (depth : List String) -> FileSystem -> List String
 11 | linearize depth (DirTree n []) = [concat $ reverse $ intersperse "/" (n :: depth)]
                                                           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Error: While processing right hand side of show. When unifying:
    List String
and:
    Vect ?len ?elem
Mismatch between: List String and Vect ?len ?elem.

fileDiff.FileDiff:16:41--16:56
 12 | linearize depth (DirTree n files) = concatMap (linearize (n :: depth)) files
 13 | linearize depth (FileTree n) = [concat $ reverse $ intersperse "/" (n :: depth)]
 14 | 
 15 | Show FileSystem where
 16 |   show fs = concat $ intersperse "\n" $ linearize [] fs
                                              ^^^^^^^^^^^^^^^

Error: While processing type of lsAcc. Undefined name Directory. 

fileDiff.FileDiff:19:9--19:18
 15 | Show FileSystem where
 16 |   show fs = concat $ intersperse "\n" $ linearize [] fs
 17 | 
 18 | ||| Ls with accumulator, uses `dirEntry` to get to the next entry
 19 | lsAcc : Directory -> Maybe (List String) -> IO (Either FileError (List String))
              ^^^^^^^^^

Error: While processing right hand side of lsAcc. While processing right hand side of lsAcc,notDot. Undefined name strHead. 

fileDiff.FileDiff:30:18--30:25
 26 |   where
 27 |     ||| Don't pay attention to files starting with a dot
 28 |     notDot : String -> Bool
 29 |     notDot "" = True
 30 |     notDot str = strHead str /= '.'
                       ^^^^^^^

Error: While processing type of ls. Undefined name FileError. 

fileDiff.FileDiff:33:27--33:36
 29 |     notDot "" = True
 30 |     notDot str = strHead str /= '.'
 31 | 
 32 | ||| List all files in a directory
 33 | ls : String -> IO (Either FileError (List String))
                                ^^^^^^^^^

Error: While processing right hand side of ls. Undefined name dirOpen. 

fileDiff.FileDiff:34:25--34:32
 30 |     notDot str = strHead str /= '.'
 31 | 
 32 | ||| List all files in a directory
 33 | ls : String -> IO (Either FileError (List String))
 34 | ls name = do Right d <- dirOpen name | Left err => pure (Left err)
                              ^^^^^^^

Error: While processing type of lsRec. Undefined name FileError. 

fileDiff.FileDiff:54:41--54:50
 50 |                  (a -> m (n d)) -> l a -> m (n (l d))
 51 | doubleTraverse f x = traverse id <$> traverse f x
 52 | 
 53 | ||| Construct a tree of all files in a directory structure
 54 | lsRec : Vect (S n) String -> IO (Either FileError FileSystem)
                                              ^^^^^^^^^

Error: No type declaration for Main.lsRec.

fileDiff.FileDiff:55:1--68:16
 55 | lsRec path@(directory :: ds) = do
 56 |     Right files <- ls (pathFromVect path) | Left err => pure (Left err)
 57 |     (dirs, files) <- partitionM (isDir path) files
 58 |     Right subTree <- doubleTraverse (\d => lsRec (d :: path)) dirs
 59 |       | Left err => pure (Left err)
 60 |     pure $ Right (DirTree directory (subTree ++ map FileTree files))

Error: While processing right hand side of fixFormat. Undefined name takeWhile. 

fileDiff.FileDiff:74:26--74:35
 70 | ||| We don't care about the begining of the file path nor the file extension
 71 | ||| The begining is the root folder, which will always be different
 72 | ||| The filepath is `lidr` for idris1 and `idr` for Idris2 so it's not helpful
 73 | fixFormat : Nat -> String -> String
 74 | fixFormat n str = pack $ takeWhile (/= '.') $ drop n $ unpack str
                               ^^^^^^^^^

Error: While processing right hand side of main. Undefined name getArgs. 

fileDiff.FileDiff:80:36--80:43
 76 | missing : Eq a => List a -> List a -> List a
 77 | missing xs ys = filter (not . flip elem ys) xs
 78 | 
 79 | main : IO ()
 80 | main = do [_, folder1, folder2] <- getArgs
                                         ^^^^^^^

Warning: compiling hole Main.main
make: *** [compare] Error 1

Define fast compose

In a free smc, you give me two morphisms f g such that the codomain of f is a permutation of the domain of g. You also give me a list of binary swaps to turn one into the other. I will figure out for you a list of morphisms h_1, ..., h_n such that each h_i has the form id tensor symmetry tensor id, and such that the composition f;h_1;..;h_n;g makes sense. Said composition is what I will give you back.

Is it possible to use non-Haskell TeX library and drop dependency on lhs2tex?

Building lhs2tex pulls in a lot of stuff, since their makefiles build apparently does not work anymore. This also means that on many platforms it will not build at all (where current GHC is broken and Cabal not supported).

There are numerous properly cross-platform TeX libraries. Can we use some of those instead?

Can't build using elba 0.3.2

When building using elba 0.3.2, idris 1.3.2, compilation always fails on MonoidalCategory.MonoidalCategory - it stops there for a long time, then fails with essentially no error message.
Trying to compile the file manually with Idris works fine.

$ elba --version
elba 0.3.2
$ idris --version
1.3.2
$ elba build
       [1/2] Resolving dependencies...
       [2/2] Building targets...
    Building statebox/idris-ct 0.1.0 (dir+/home/eigil/projects/idris-ct) [3605e7ee..]
   Compiling Basic.Category [statebox/idris-ct]
   Compiling Basic.ConstantFunctor [statebox/idris-ct]
   Compiling Basic.Functor [statebox/idris-ct]
   Compiling Basic.Isomorphism [statebox/idris-ct]
   Compiling Basic.NaturalIsomorphism [statebox/idris-ct]
   Compiling Basic.NaturalTransformation [statebox/idris-ct]
   Compiling Cats.CatsAsCategory [statebox/idris-ct]
   Compiling Cats.FunctorsAsCategory [statebox/idris-ct]
   Compiling CoLimits.CoCone [statebox/idris-ct]
   Compiling CoLimits.CoConeCat [statebox/idris-ct]
   Compiling CoLimits.CoLimit [statebox/idris-ct]
   Compiling CoLimits.CoLimitAsInitialObject [statebox/idris-ct]
   Compiling CoLimits.CoProduct [statebox/idris-ct]
   Compiling CoLimits.InitialObject [statebox/idris-ct]
   Compiling CoLimits.InitialObjectAsCoLimit [statebox/idris-ct]
   Compiling CoLimits.Pushout [statebox/idris-ct]
   Compiling CommutativeDiagram.Diagram [statebox/idris-ct]
   Compiling Discrete.DiscreteCategory [statebox/idris-ct]
   Compiling Discrete.FunctionAsFunctor [statebox/idris-ct]
   Compiling Dual.DualCategory [statebox/idris-ct]
   Compiling Dual.DualFunctor [statebox/idris-ct]
   Compiling Empty.EmptyCategory [statebox/idris-ct]
   Compiling Empty.EmptyFunctor [statebox/idris-ct]
   Compiling Free.FreeFunctor [statebox/idris-ct]
   Compiling Free.Graph [statebox/idris-ct]
   Compiling Free.Path [statebox/idris-ct]
   Compiling Free.PathCategory [statebox/idris-ct]
   Compiling Idris.EitherAsCoProduct [statebox/idris-ct]
   Compiling Idris.FunctorAsCFunctor [statebox/idris-ct]
   Compiling Idris.TypesAsCategory [statebox/idris-ct]
   Compiling Idris.TypesAsCategoryExtensional [statebox/idris-ct]
   Compiling Lens.Lens [statebox/idris-ct]
   Compiling Lens.SimpleLens [statebox/idris-ct]
   Compiling Limits.Limit [statebox/idris-ct]
   Compiling Limits.Pullback [statebox/idris-ct]
   Compiling Limits.TerminalObject [statebox/idris-ct]
   Compiling Monad.IOMonad [statebox/idris-ct]
   Compiling Monad.KleisliCategory [statebox/idris-ct]
   Compiling Monad.Monad [statebox/idris-ct]
   Compiling Monad.VerifiedMonadAsMonad [statebox/idris-ct]
   Compiling Monoid.Monoid [statebox/idris-ct]
   Compiling Monoid.MonoidAsCategory [statebox/idris-ct]
   Compiling Monoid.MonoidMorphism [statebox/idris-ct]
   Compiling Monoid.MonoidMorphismAsFunctor [statebox/idris-ct]
   Compiling Monoid.MonoidsCategory [statebox/idris-ct]
   Compiling MonoidalCategory.MonoidalCategory [statebox/idris-ct]
     [error] Couldn't build library target for statebox/idris-ct 0.1.0 (dir+/home/eigil/projects/idris-ct)
> "idris" "--check" "-p" "contrib" "MonoidalCategory/MonoidalCategory.lidr"


error: one or more packages couldn't be built

build times

Building takes quite a long time and lately has been failing on my measly 2GB ram machine.

Is there a way to have an idris project depend on a pre-compiled target, and a way to publish these targets for the current master branch?

implement Kleisli category

given a category and a monad (which needs to be defined first), define the Kleisli category

coming from statebox/idris-stbx-core#29

Fast compose when types are different

You give me two morphisms f, g such that domain of g is a permutation of codomain of f, with no repeated generators. I will use #17 to figure out how to turn one into the other and #18 to give you the composition of f and g.

Define operations on commutative diagrams

Provide an easy interface to work with commutative diagrams, so that it is easy to compose them

Build with idris2 fails: `Uncaught error: Error: Can't recognise token`

Running idris2 --build ./idris-ct.ipkg does not seem to work:

--->  Building idris-ct
Uncaught error: Error: Can't recognise token.

"idris-ct.ipkg":3:1--3:2
 1 | package idris-ct
 2 | 
 3 | {-
     ^

Command failed: /opt/local/bin/idris2 --build /opt/local/var/macports/build/_opt_svacchanda_SonomaPorts_math_idris-ct/idris-ct/work/idris-ct-fbc7f633e0d86bfe5b56a2c4b9db6f780d59106d/idris-ct.ipkg
Exit code: 1

Am I doing something wrong? --checkpkg is not recognized at all.

find a way to specify a functor from a graph category to the category of types and functions

We can build the free category over a graph. Sending vertices to types and edges to functions among those types should allow us to functorially map the graph category to the category of types and functions.

we need to find a way to make this functor description serializable (probably this could be done in a second step)

category of lenses

pedagogically adding some non trivial structure

Not sure if it fits here, but I was looking at this library and wanted to see how to, say, add the definition of 2-categories as a test case.

Now it can be done with all the elementary pieces (whiskering, interchange, etc..) but trying to do it abstractly (with a composition functor etc) leads to interesting (easy but not trivial) parts which are currently missing.

Say, the iso in Cat between a category A and 1 * A, proving equalities of functors (?).
Those kind of things are great opportunities for pedagogical material. Not trivial stuff. But not too hard.

I would very much like to see some experienced user adding those in a twitch / youtube / in person. That would be ideal to further develop this nice library.

Or maybe there are similar content in the same vein someone could recommend ?

Thanks in advance

prove that the category of types and functions is symmetric monoidal

Reinstate documentation generation

This has become broken when we split off this repo.

Use categorical components to actually compute things

write a function that takes a graph, an initial state (a vertex), an initial value (of the type defined by the vertex), a functor from the path category to the category of types and functions, a path in the graph and computes something

Define IO monad

Define the IO monad or some other monad which would allow us to actually perform some real world computation through the Kleisli category

Builds a path of a graph from a list of edges

given a list of edges of a graph (possibly as a list of pairs of vertices, or some other easily serialisable format), check if they are consecutive and in that case return a path in the graph

define smproc category

in https://github.com/jameshaydon/smproc there is defined a monoidal category. Integrate it with out definitions

coming from statebox/idris-stbx-core#30

Add INSTALL instructions in README.md

It would be useful to explain in README.md how to install this package as a dependency for another Idris project.

Day convolution

provide the setting for a formal proof of https://mathoverflow.net/questions/346529/the-convolution-of-comonads-is-a-comonad

Finish up wiring diagram

coming from statebox/idris-stbx-core#28

Why is NaturalIsomorphism implemented as a separate type rather than as Isomorphism in the functor category?

Is there a particular reason why

NaturalIsomorphism 
  (cat1 : Category)  
  (cat2 : Category) 
  (fun1 : CFunctor cat1 cat2)  
  (fun2 : CFunctor cat1 cat2)

isn't simply implemented as

Isomorphism (functorCategory cat1 cat2) fun1 fun2

where Isomorphism record is defined as:

record Isomorphism (cat : Cat) (a : obj cat) (b : obj cat) where
  constructor MkIso
  forward : hom cat a b
  inverse : hom cat b a
  rightInverse : o cat {a=a} {b=b} {c=a}              inverse forward === idd cat {a=a}
  leftInverse  :  o cat {a=b} {b=a} {c=b} forward inverse              === idd cat {a=b}

It seems to be a simplification and allows us to talk about all sorts of Isomorphisms in different categories.
For example, monoidal categories look slightly different.
The reason for slightly different function names is because I'm implementing a ct libary as well here.

Define free categories over graphs

Javascript, the good parts

As discussed in dev call,

after implementing #34 we want to call out to JS FFI and compile the Idris code to JS so that can run a morphism it as a JS function

Define useful tactics

Convert to Idris 2

We will have to consider this at some point, so I thought it would be good to put this out here.

coming from statebox/idris-stbx-core#34

Define adjunctions

Define free symmetric monoidal category

improve compilation speed for ProductCategory

this is slowing down the compilation of all the monoidal part of the library

coming from statebox/idris-stbx-core#32

add LICENSE and CLA

Define list ordering with a target in Idris

You give me two lists such that one is the permutation of the other. I give you a list of binary swaps which turn the first list into the other.

Make nix-shell build great again

Jelle:

we should probably just update default.nix
rename idris-stbx-core to idris-ct

Build error with idris 1.3.2

When running idris --build idris-ct.ipkg (or idris --checkpkg idris-ct.pkg), the build fails on CoLimits/CoProduct.lidr with the following error :

Entering directory `./src'
Type checking ./CoLimits/CoProduct.lidr
./CoLimits/CoProduct.lidr:83:5-97:48:
   |
83 | >   let
   |     ~~~ ...
When checking right hand side of composeCoProductMorphisms with expected type
        CommutingMorphism cat l r (carrier a) (carrier a) (inl a) (inr a) (inl a) (inr a)

When checking argument commutativityLeft to constructor CoLimits.CoProduct.MkCommutingMorphism:
        No such variable rewrite__impl

./CoLimits/CoProduct.lidr:119:5-133:66:
    |
119 | >   let
    |     ~~~ ...
When checking right hand side of coProductsAreIsomorphic with expected type
        Isomorphic cat (carrier a) (carrier b)

When checking an application of function Basic.Isomorphism.buildIsomorphic:
        rewriting challenger (composeCoProductMorphisms cat l r a b) to challenger (exists a (carrier a) (inl a) (inr a)) did not change type compose cat
                                                                                                                                                      (carrier a)
                                                                                                                                                      (carrier b)
                                                                                                                                                      (carrier a)
                                                                                                                                                      (challenger (exists a (carrier b) (inl b) (inr b)))
                                                                                                                                                      (challenger (exists b (carrier a) (inl a) (inr a))) =
                                                                                                                                              identity cat (carrier a)

This is on master, on NixOS.

$ idris --version
1.3.2

A quick search lead me to the following issue idris-lang/Idris-dev#4254 which seems to be related to the second error.

Can't build using elba

Hi,

I'm trying to build this project using the package manage elba and failing to do so.
Literally after doing git clone, cd-ing into the project and running elba build I get the following error:

>>> elba build
       [1/2] Resolving dependencies...

       [2/2] Building targets...
    Building statebox/idris-ct 0.1.0 (dir+/home/bgavran/code/idris-ct) [ef9b30a8..]
     [error] Couldn't build library target for statebox/idris-ct 0.1.0 (dir+/home/bgavran/code/idris-ct)
[cmd] "idris" "--check" "-p" "contrib" "Basic/Category.idr" "Basic/Functor.idr" "Basic/Isomorphism.idr" "Basic/NaturalIsomorphism.idr" "Basic/NaturalTransformation.idr" "Cats/CatsAsCategory.idr" "Discrete/DiscreteCategory.idr" "Discrete/FunctionAsFunctor.idr" "Dual/DualCategory.idr" "Dual/DualFunctor.idr" "Idris/FunctorAsCFunctor.idr" "Idris/TypesAsCategory.idr" "Idris/TypesAsCategoryExtensional.idr" "Monoid/Monoid.idr" "Monoid/MonoidAsCategory.idr" "Monoid/MonoidMorphism.idr" "Monoid/MonoidMorphismAsFunctor.idr" "Monoid/MonoidsCategory.idr" "MonoidalCategory/MonoidalCategory.idr" "MonoidalCategory/MonoidalCategoryHelpers.idr" "MonoidalCategory/StrictMonoidalCategory.idr" "MonoidalCategory/SymmetricMonoidalCategory.idr" "MonoidalCategory/SymmetricMonoidalCategoryHelpers.idr" "PointedTypes/PointedTypesAsCategory.idr" "Preorder/MonotoneMap.idr" "Preorder/MonotoneMapAsFunctor.idr" "Preorder/PreorderAsCategory.idr" "Preorder/UniquePreorder.idr" "Product/ProductCategory.idr" "Product/ProductFunctor.idr" "Utils.idr"
 Can't find import Basic/Category.idr


error: one or more packages couldn't be built

I notice everything is a literate idris file and elba is trying to import .idr instead of perhaps .lidr?

Solve timeout problem with Travis

my idea is to add a --log 1 in the build process so there is continuous output and Travis does not stop.

This implies modifying the build-idris-package nix package

Boolean category

In my Data.Category project I found the (pre)order of booleans to be a nice category as a testbed to implement concepts in.

define f-algebras and eilenberg-moore category

type checker hangs when checking symmetric monoidal category associator

at the moment the associator does not work for some mysterious reason. Find out why and fix it

• issue on idris-lang #4690

close stale issues and PRs

make the implicitable implicit

one of the big complaints of the current state of the library is that many arguments which could be implicit are not.

Try to refactor to actually make them implicit

Fast compose with same types

Like #19 but now we allow repeated generators in the object. The users should be able to specify if they want the same generators to be swapped, and how. If they do not specify anything, then fastcompose should compose f and g without swapping the same object. This is analogous to "swapfree" symmetries in https://arxiv.org/abs/1904.12974 .
I know this specifications suck a bit, but they are a starting point to make clear what is that we want to achieve conceptually :)

Define a category of spans