Icelandjack

Embedding F with a twist.

Icelandjack

Reddit discussion

Continuation of Encoding Overlapping, Extensible Isomorphisms: encoding "open kinds" to better express some awkward type classes.

Icelandjack

• Continued in Explicit Witnesses of Monoid Actions, Semigroup / Monoid / Applicative homomorphisms

Reddit discussion

My initial motivation for -XDerivingVia was deriving across isomorphisms.

Standard type-class encodings of isos turn out to be awkward due to overlap.

Icelandjack

{-# Language StandaloneDeriving, PatternSynonyms, GADTs, UndecidableInstances, ScopedTypeVariables, TemplateHaskell, TypeInType, TypeOperators, TypeFamilies, AllowAmbiguousTypes, InstanceSigs, TypeApplications #-}

import Data.Singletons
import Data.Singletons.Prelude.Base
import Data.Singletons.TH
import Data.Kind
import Control.Arrow ((***))

data Dup :: Type ~> Type

Icelandjack

Free Categories

You can build categories just by connecting objects with arrows. You can imagine starting with any directed graph and making it into a category by simply adding more arrows. First, add an identity arrow at each node. Then, for any two arrows such that the end of one coincides with the beginning of the other (in other words, any two composable arrows), add a new arrow to serve as their composition. Every time you add a new arrow, you have to also consider its composition with any other arrow (except for the identity arrows) and itself. You usually end up with infinitely many arrows, but that’s okay.

Another way of looking at this process is that you’re creating a category, which has an object for every node in the graph, and all possible chains of composable graph edges as morphisms. (You may even consider identity morphisms as special cases of chains of length zero.)

Such a category is called a free category generated by a given graph. It’s an example of a free construction, a proces

Icelandjack

http://www.michaelburge.us/2017/09/27/delta-debugging-in-haskell.html

data HList f xs where
  HNil  :: HList f '[]
  HCons :: f a -> HList f as -> HList f (a ': as)

divideGeneral :: forall f a bs. Divisible f => (a -> HList Identity bs) -> (HList f bs -> f a)
divideGeneral f = \case
  HNil ->

Icelandjack

This would be sweet to have:

instance Category cat => Monoid (Join cat a) where
  mempty = Join id

  Join f `mappend` Join g = Join (f . g)

and where we can define

Icelandjack

Type classes in terms of row types

type Semigroup s = { Monoid s with mappend :: s -> s -> s | _ }

type Pointed f = { Applicative f with pure  :: forall a. a -> f a | _ }
type Apply   f = { Applicative f with (<*>) :: forall a b. f (a -> b) -> f a -> f b | _ }
type Bind    m = { Monad       m with (>>=) :: forall a b. m a -> (a -> m b) -> m b | _ }

Icelandjack

{-# LANGUAGE StaticPointers #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Data.Binary
import Data.Typeable
import System.IO.Unsafe
import GHC.StaticPtr

Icelandjack

reddit discussion

IxMonad implies Monad for (EDIT: Exists as LowerIx with newtype LiftIx m i j a = LiftIx (m a))

and `

newtype Same :: (k -> k -> k' -> Type) -> (k -> k' -> Type) where
  Same :: p f f a -> Same p f a