Icelandjack

To allow hask

type Cat k = k -> k -> Type

type Fun i j = i -> j

data Nat :: Cat i -> Cat j -> Cat (Fun i j) where
  Nat :: (FunctorOf cat cat' f, FunctorOf cat cat' f') => (forall a. Ob cat a => cat' (f a) (f' a)) -> Cat cat cat' f f'

Icelandjack

Motivating examples for https://ghc.haskell.org/trac/ghc/ticket/10843, https://ghc.haskell.org/trac/ghc/wiki/ArgumentDo

This should allow

curry $ \case

without the dollar giving us weird code

Icelandjack

http://www.cs.ox.ac.uk/people/bob.coecke/AbrNikos.pdf

Why study categories—what are they good for? We can offer a range of answers for readers coming from different backgrounds:

• For mathematicians: category theory organises your previous mathematical experience in a new and powerful way, revealing new connections and structure, and allows you to “think bigger thoughts”.
• For computer scientists: category theory gives a precise handle on important notions such as compositionality, abstraction, representationindependence, genericity and more. Otherwise put, it provides the fundamental mathematical structures underpinning many key programming concepts.
• For logicians: category theory gives a syntax-independent view of the fundamental structures of logic, and opens up new kinds of models and interpretations.
• For philosophers: category theory opens up a fresh approach to structuralist foundations of mathematics and science; and an alternative to the traditional focus on set theory
• For **p

Icelandjack

Free category is ubiquitous

https://github.com/kylcarte/derivation/blob/21776455a80c57db14276a6477486fc78cf9018f/src/Data/Evaluation.hs#L26

Icelandjack

https://github.com/phadej/metametapost/tree/34eb0d757655d15317d58f549e9cf4c794cff79e/src/MetaMetaPost

• https://github.com/phadej/metametapost/blob/34eb0d757655d15317d58f549e9cf4c794cff79e/src/MetaMetaPost/Simplifier.hs

simplify :: Expr SomePrim (Type s) a -> Either String (MP s a)
simplify (Var a)                = pure (MPApp (MPVar a))
simplify (Prim (SomePrim p))    = simplifyPrim0 p
simplify (Lam _ _)              = throwError "Non-applied lambda abstraction"

Icelandjack

mniip
edwardk, I think I just came up with the most complicated solution to the Show1 problem 
phadej
Show1 problem? 
mniip
instance Show (IdentityT m a) where ??? 
phadej
and your solution is? 
mniip
coming up 

Icelandjack

Interesting https://www.reddit.com/r/haskell/comments/1u8rp1/with_two_different_functors/

Description of monoidal natural transformations https://gist.github.com/Icelandjack/9e6902690a244286843164e554a8c3db

Icelandjack

https://mail.haskell.org/pipermail/haskell-cafe/2010-November/086055.html

http://conal.net/blog/posts/simplifying-semantics-with-type-class-morphisms

http://conal.net/blog/posts/another-lovely-example-of-type-class-morphisms

https://arxiv.org/pdf/1202.2919.pdf

eta (pure c) = pure c

Icelandjack

{-# Language InstanceSigs, ViewPatterns, TupleSections, GeneralizedNewtypeDeriving, TemplateHaskell, LambdaCase #-}

module D where

import Language.Haskell.TH
import Data.Coerce

deriveVia :: Name -> Name -> Name -> Q [Dec]
deriveVia className ty viaNewTy = do
  a <- reify className

Icelandjack

Principle of identity expansion

Whenever some construction has a certain relationship to all constructions of the same kind within a category, it must, in particular, have this relationship to itself. Socrates’ dictum to “know thyself” is as important in category theory as it is in life. So whenever we encounter a universal construction we will see what we can learn about it by “probing it with itself”. In the case of a terminal object, this means choosing X ≔ T in the definition.

Lemma 3.1.1.2 (identity expansion for terminals) If T is a terminal object then !(T) = id(T).

Lemma 3.1.4.2 (identity expansion for initials) If S is an initial object then ¡(S) = id(S).