Skip to content

Instantly share code, notes, and snippets.

View Icelandjack's full-sized avatar

Icelandjack

198 followers · 7 following
View GitHub Profile
@Icelandjack
Icelandjack / 14048.markdown
Created August 3, 2017 01:27
#14048: Data instances of kind Constraint

Hask

LiftC1 :: (k1 -> k2 -> Constraint) -> (k -> k1) -> (k -> k2) -> (k -> Constraint)
Lift1  :: (k1 -> k2 -> Type)       -> (k -> k1) -> (k -> k2) -> (k -> Type)

LiftC2 :: (k1 -> k2 -> k' -> Constraint) -> (k -> k1) -> (k -> k2) -> (k -> k' -> Constraint)
Lift2  :: (k1 -> k2 -> k' -> Type)       -> (k -> k1) -> (k -> k2) -> (k -> k' -> Type)
@Icelandjack
Icelandjack / RecordPatternDictionary.markdown
Last active August 7, 2017 09:09
Open Monad dictionary with record pattern synonym (and as patterns) 
{-# Language PatternSynonyms #-}
{-# Language ViewPatterns    #-}

data DMonad m = DMonad
  (forall a.   a -> m a)
  (forall a b. m a -> (a -> m b) -> m b)
  (forall a.   String -> m a)

pattern Open :: (forall a. a -> [a]) -> (forall a a'. [a] -> (a -> [a']) -> [a']) -> (forall a. String -> [a]) -> xxx
@Icelandjack
Icelandjack / ASCII.markdown
Created August 8, 2017 09:03
ASCII art
@Icelandjack
Icelandjack / pdf.markdown
Created August 8, 2017 09:44
PDF
@Icelandjack
Icelandjack / Lens.markdown
Created August 18, 2017 09:10
Lens
@Icelandjack
Icelandjack / Stuff.markdown
Last active August 24, 2017 09:29
TODO: Stuff
@Icelandjack
Icelandjack / ShootingStar.md
Last active August 25, 2017 14:42
Playing around with GHC Trac ticket #12369

Are these examples of

Application

data App0 :: Type -> Type where
  App0 :: a -> App0
@Icelandjack
Icelandjack / Binary.hs
Created September 1, 2017 09:37 — forked from ndmitchell/Binary.hs
Binary existentials
{-# LANGUAGE StaticPointers #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ScopedTypeVariables #-}
import Data.Binary
import Data.Typeable
import System.IO.Unsafe
import GHC.StaticPtr
@Icelandjack
Icelandjack / Paper.md
Created September 23, 2017 16:52
Paper: Stuff that has to be mentioned

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
Icelandjack / CCC.md
Last active October 2, 2017 07:59
CCC talking points

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