TODO: Stuff

Stuff.markdown

Free category is ubiquitous

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

Interesting allowing dotW :: EqC hom b b' -> hom b' c -> hom a b -> hom a c.

https://github.com/DrNico/alt-base/blob/3fbcd29992b5022f2a02e3e9f49154710310014d/Alt/Abstract/Category.hs

{- | General class of Categories, with two associated types: a type of Objects
and an Equivalence of Objects.
Instances must satisfy the following laws:
prop> f . (idC (source f)) == f
prop> (idC (target g)) . g == g
prop> h . (g . f) == (h . g) . f
prop> g . f == bottom "if and only if" idS g `idEq` idT f
-}
class Category hom where
    type EqC hom a b :: *
    type Obj hom a   :: *

    -- | Get the source of the morphism.
    source  :: hom a b -> Obj hom a

    -- | Get the target of the morphism.
    target  :: hom a b -> Obj hom b

    -- | Build an identity morphism over the given object.
    idC     :: Obj hom a -> hom a a

    -- | Composition with a witness obtained from the Equivalence class.
    dotW    :: EqC hom b b'
            -> hom b' c -> hom a b
            -> hom a c

data a :~: b where
  Refl :: a :~: a

instance Category (->) where
    type EqC (->) a b = a :~: b
    type Obj (->) a   = Proxy a

    source  :: (a -> b) -> Proxy a
    source _ = Proxy 

    target :: (a -> b) -> Proxy b
    target _ = Proxy

    idC :: Proxy a -> (a -> a)
    idC Proxy = \x -> x

    dotW :: b:~:b' -> (b' -> c) -> (a -> b) -> (a -> c)
    dotW Refl = \g f -> \x -> g (f x)

data a :=: b where
  Equal :: Eq a => a -> a :=: a

instance Category (,) where
    type EqC (,) a b = a :=: b
    type Obj (,) a   = a

    source :: (a, b) -> a
    source = fst

    target :: (a, b) -> b
    target = snd

    idC :: a -> (a, a)
    idC = join (,)

    dotW :: b:=:b' -> (b', c) -> (a, b) -> (a, c)
    dotW Equal{} (_, c) (a, _) = (a, c)

https://github.com/DrNico/alt-base/blob/3fbcd29992b5022f2a02e3e9f49154710310014d/Alt/Category/Set.hs

instance Category CatSet where
    type EqC CatSet a b = EqSet (ObjSet a) (ObjSet b)
    type Obj CatSet a   = ObjSet a

    source (FuncSet s _ _) = ObjSet s
    target (FuncSet _ _ t) = ObjSet t

    idC (ObjSet o) = FuncSet {
        domSet = o,
        arrSet = zipWith (\_ i -> i) o (iterate (+ 1) 0),
        codSet = o
    }

    dotW refl = dot
        where
            dot (FuncSet sg g tg) (FuncSet sf f tf) =
                FuncSet sf (map ((!!) g) f) tg

https://github.com/msp-strath/ZEUG/blob/66b09b125a226b0c5a4b89b302e8855892554abe/April17/Utils.hs
https://github.com/msp-strath/ZEUG/blob/66b09b125a226b0c5a4b89b302e8855892554abe/April17/OPE.hs

https://gist.github.com/gallais/12e5ff1015fd28a6fce8c693f8b59a3d

Small well-scoped and well-typed by construction imperative DSL

ghc-proposals/ghc-proposals#6

SPJ Simon Peyton Jones

I have always been unsettled by the super-polymorphic type for lenses. I would far prefer them to have an proper abstract type (Lens s t ab). But the implicit subtyping we get through exposing the representation is truly amazing and truly useful. I am uneasy about the tension between abstraction and utility, and I hope we may ultimately figure out a better way to reconcile them. Are Reid's suggestions above a start?

Example of my standardising lesser used fixity / operators from

infixl 4 <?>

-- | infix form of `fromMaybe`.
(<?>) :: Maybe a -> a -> a
Just a <?> _ = a
_      <?> a = a

UndecidableSuperClasses

to implement indexed profunctor lenses

{-# Language UndecidableSuperClasses #-}

class (Unindexed cat ~ Unindexed (Unindexed cat), Indexable index (Unindexed cat)) => Indexable index cat where
  type Unindexed cat :: k -> k' -> Type

  indexed :: cat a b
          -> index -> Unindexed cat a b

instance Indexable index (->) where
  type Unindexed (->) = (->)

  indexed :: forall a b.
                (a -> b)
    -> (index -> a -> b)
  indexed = const @(a -> b) @index

newtype Indexed i a b = Indexed { runIndexed :: i -> a -> b }

instance index ~ j => Indexable index (Indexed j) where
  type Unindexed (Indexed j) = (->)

  indexed :: Indexed index a b
          -> (index -> a -> b)
  indexed = runIndexed

type IndexedTraversal index s t a b = forall p.
  (Indexable index p, Traversing p, Traversing (Unindexed p)) =>
    p a b -> Unindexed p s t

foo :: IndexedTraversal Int a b [a] [b]
foo = undefined

bar :: IndexedTraversal Int a b [[[[a]]]] [[[[b]]]]
bar = foo.foo.foo.foo

TypeFamilyDependencies

https://github.com/mvr/optics/blob/34080e6cb5ad6017b8eb8cfb8d5402e3e9964874/src/NewTest.hs

class Action (c :: (* -> *) -> Constraint) where
  type Wanderer c (a :: *) (b :: *) = (p :: * -> * -> *) | p -> c a b
  type Wanderer c a b = LoneWanderer c a b

generic-transformation transformer

fmap : (b. Term b => b -> b) -> (b. Term b => b -> b)

https://www.microsoft.com/en-us/research/wp-content/uploads/2003/01/hmap.pdf

6 Refinements and reflections

Having introduced the basics, we pause to reflect on the ideas a little and to make some modest generalisations.

6.1 An aside about types

It is worth noticing that the type of everywhere could equivalently
be written thus:

everywhere :: (forall b. Term b => b -> b) -> (forall a. Term a => a -> a)

by moving the implicit forall a inwards. The nice thing about writing it this way is that it becomes clear that everywhere is a generic-transformation transformer. We might even write this:

type GenericT = forall a. Term a => a -> a
everywhere :: GenericT -> GenericT

The same approach gives a more perspicuous type for everything:

type GenericQ r = forall a. Term a => a -> r
everything :: (r -> r -> r) -> GerericQ r -> GerericQ r

A tutorial on the universality and expressiveness of fold

uses

fold :: (α → β → β) → β → ([α] → β)

instead of

fold :: (a -> b -> b) -> b -> [a] -> b
-- or
fold :: (a -> b -> b) -> (b -> [a] -> b)