Skip to content

Instantly share code, notes, and snippets.

@Icelandjack
Icelandjack / ComonadVia.hs
Created Mar 8, 2019
DerivingVia (Co Any Pair) and (Co All Pair)
View ComonadVia.hs
{-# Language DeriveFunctor #-}
{-# Language DerivingVia #-}
{-# Language FlexibleContexts #-}
{-# Language FlexibleInstances #-}
{-# Language GADTs #-}
{-# Language GeneralizedNewtypeDeriving #-}
{-# Language InstanceSigs #-}
{-# Language ScopedTypeVariables #-}
{-# Language TypeApplications #-}
{-# Language TypeFamilies #-}
@Icelandjack
Icelandjack / Kleisli_Category.hs
Last active Jan 6, 2019
Kind-indexed Category instance for Kleisli
View Kleisli_Category.hs
-- https://www.reddit.com/r/haskell/comments/abxem5/experimenting_with_kleisli_instance_of/
{-# Language TypeApplications #-}
{-# Language RankNTypes #-}
{-# Language DataKinds #-}
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
{-# Language TypeOperators #-}
{-# Language GADTs #-}
{-# Language TypeFamilies #-}
@Icelandjack
Icelandjack / ZipWith.markdown
Last active Dec 29, 2018
Variable-arity zipWith in terms of Applicative ZipList
View ZipWith.markdown

I was implementing "variable-arity zipWith" from Richard Eisenberg's thesis (recommended) when I noticed it used

apply :: [a -> b] -> [a] -> [b]
apply (f:fs) (a:as) = f a : apply fs as
apply _      _      = []

and

repeat :: a -> [a]
@Icelandjack
Icelandjack / Yoneda_II.markdown
Last active Aug 21, 2021
Yoneda Intuition from Humble Beginnings
View Yoneda_II.markdown

(previous Yoneda blog) (reddit) (twitter)

Yoneda Intuition from Humble Beginnings

Let's explore the Yoneda lemma. You don't need to be an advanced Haskeller to understand this. In fact I claim you will understand the first section fine if you're comfortable with map/fmap and id.

I am not out to motivate it, but we will explore Yoneda at the level of terms and at the level of types.

View Buggy_Program.hs
{-# Language RankNTypes #-}
{-# Language LambdaCase #-}
{-# Language TypeOperators #-}
{-# Language TypeApplications #-}
{-# Language PolyKinds #-}
{-# Language TypeFamilies #-}
{-# Language FlexibleInstances #-}
{-# Language GADTs #-}
{-# Language ConstraintKinds #-}
{-# Language MultiParamTypeClasses #-}
View Yoneda.markdown
import Data.Functor.Yoneda
import Data.Char
import Data.Kind

infixr 5
  ·

type  List :: (Type -> Type) -> Constraint
class List f where
View Inj.markdown
data Kl_kind :: (Type -> Type) -> Type where
  Kl :: Type -> Kl_kind(m)
  
type family
  UnKl (kl :: Kl_kind m) = (res :: Type) | res m -> kl where
  UnKl (Kl a) = a
View Notation.markdown

Non-standard operators I use :) linked to from my twitter profile

I use kind synonyms

type T   = Type
type TT  = T -> T
type TTT = T -> TT
type C   = Constraint
type TC  = T -> C
@Icelandjack
Icelandjack / Braindump.hs
Last active Oct 15, 2018
For Chris Allen, braindump
View Braindump.hs
-- type Sig k = [k] -> Type
--
-- data AST :: Sig k -> Sig k where
-- Sym :: dom a -> AST dom a
-- (:$) :: AST dom (a:as) -> AST dom '[a] -> AST dom as
singletons [d| data N = O | S N |]
infixr 5
data Vec :: N -> Type -> Type where
View SystemF.hs
-- SYSTEM F
-- http://homepages.inf.ed.ac.uk/slindley/papers/embedding-f.pdf
--
-- Type-level lambdas
-- https://gist.github.com/AndrasKovacs/ac71371d0ca6e0995541e42cd3a3b0cf
{-# language TemplateHaskell, ScopedTypeVariables, RankNTypes,
TypeFamilies, UndecidableInstances, DeriveFunctor, GADTs,
TypeOperators, TypeApplications, AllowAmbiguousTypes,