Skip to content

Instantly share code, notes, and snippets.

@Icelandjack
Icelandjack / Code.markdown
Created Jun 2, 2017
TODO: Look at when on laptop
View Code.markdown
View Trac_10843.markdown
View ImplicationConstraints.markdown

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
Icelandjack / id.markdown
Last active Jun 25, 2017
Identity function, id :: a -> a
View id.markdown

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).

@Icelandjack
Icelandjack / Deriving.hs
Last active Jul 2, 2017
Template Haskell deriving, first implementation
View Deriving.hs
{-# 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
Icelandjack / ThinkingAbout.markdown
Created Jul 14, 2017
[TALK,BLOG,QUOTE] Different ways of thinking about
View ThinkingAbout.markdown

Compare https://twitter.com/mrkgnaow/status/876007524968800256 to Haskell, should probably stress this before each talk

This is a list of different ways of thinking about or conceiving of the derivative, rather than a list of different logical definitions. Unless great efforts are made to maintain the tone and flavor of the original human insight, the differences start to evaporate as soon as the mental concepts are translated into precise, formal and explicit definitions.

I can remember absorbing each of those concepts as something new and interesting, and spending a good deal of mental time and effort digesting and practicing with each, reconciling it with the others. I also remember coming back to revisit these different concepts later with added meaning and understanding.

@Icelandjack
Icelandjack / checkiffails.hs
Created Jul 14, 2017
See if this still fails on GHC 8.2
View checkiffails.hs
type Cat k = k -> k -> Type
data T = D | I
type family
Interp (a :: T) :: Type where
Interp I = Int
Interp D = Double
data Fn :: (T, T) -> Type where
View teaching.markdown

http://www.eduhk.hk/cte2017/doc/CTE2017%20Proceedings.pdf#page=138

Computational thinking has attracted a lot of attention worldwide in recent years since the publication of Jeannette M. Wing’s (2006) highly influential paper in the Communications of the ACM, in which she argues that the way computer scientists think about the world is useful in other contexts. Wing writes:

Computational thinking involves solving problems, designing systems, and understanding human behavior, by drawing on the concepts fundamental to computer science. Computational thinking includes a range of

@Icelandjack
Icelandjack / 12001.markdown
Last active Jul 27, 2017
GHC Trac #12001: Add pattern synonyms to base
View 12001.markdown

Ticket #12001.

Data.List.NonEmpty

pattern Singleton :: a -> NonEmpty a
pattern Singleton a <- (uncons -> (a, Nothing))
  where Singleton a = a N.:| []

infixr 5 :|