Skip to content

Instantly share code, notes, and snippets.

@Icelandjack
Icelandjack / Product_of_Codes.hs
Created July 30, 2022 05:20
Implement product of datatypes in generics-sop: liftA2 (++) of codes
-- This witnesses multiplying two polynomials
--
-- Code (Maybe a) = [[], [a]]
-- Code (Maybe b) = [[], [b]]
--
-- Then the product of (Maybe a, Maybe b) is isomorphic to the
-- multiplication of their codes
--
-- Code (MegaMaybe a b) = [[], [a], [b], [a,b]]
--
@Icelandjack
Icelandjack / Applicative.hs
Created April 9, 2022 13:02
Idiomatically
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
@Icelandjack
Icelandjack / Applicative_Sum.hs
Last active October 16, 2021 14:34
Deriving Applicative for sums of functors
type f ~> g = (forall x. f x -> g x)
infixr 0 ··>
type (··>) :: (Type -> Type) -> (Type -> Type) -> Type
type f ··> g = Proxy '(f, g) -> Type
type Idiom :: f ··> g -> Constraint
class Idiom (hom :: f ··> g) where
idiom :: f ~> g
@Icelandjack
Icelandjack / nary_composition.agda
Last active October 11, 2021 12:23
Dependent polyvariadic mixfix function composition in Agda
infixr 80 _◦_
_◦_ : forall {l1 l2 l3 : Level }
{A : -> Set l1}
{B : A -> Set l2}
{C : (a : A) -> B a -> Set l3}
(g : {a : A} -> (b : B a) -> C a b )
(f : (a : A) -> B a)
-> (a : A) -> C a (f a)
g ◦ f = \a -> g (f a)
@Icelandjack
Icelandjack / Generics_Distr.hs
Created August 13, 2021 21:14
Simplify and Distribute GHC.Generics
norm :: Generic1 f => Summs (Rep1 f) => f ~> Summ (Rep1 f) Zero
norm as = summs (from1 as) (Proxy @Zero)
class Summs rep where
type Summ rep (end :: Type -> Type) :: Type -> Type
summs :: rep a -> Proxy end -> Summ rep end a
skips :: Proxy rep -> end a -> Summ rep end a
instance Summs Zero where
@Icelandjack
Icelandjack / classless.hs
Last active July 13, 2021 18:38
Classless GHC.Generics with Type.Reflection
{-# Language EmptyCase #-}
{-# Language GADTs #-}
{-# Language InstanceSigs #-}
{-# Language PatternSynonyms #-}
{-# Language PolyKinds #-}
{-# Language ScopedTypeVariables #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeApplications #-}
{-# Language TypeFamilies #-}
{-# Language TypeOperators #-}
@Icelandjack
Icelandjack / Functor.hs
Last active October 10, 2020 16:06
Functor
{-
Every functor is a function mapping categories.
I want to specify them all in one place,
instance Functor (->) where
type Arr (->) = (<–) :- (->) :- End (->)
without having to specified partial applications of it
@Icelandjack
Icelandjack / circ.hs
Created October 3, 2020 11:40
Tree instance for Ap and Biap
instance (Applicative f, Treey tree) => Treey (Ap f tree) where
leaf :: Int -> Ap f tree
leaf = pure . leaf
(¦) :: Ap f tree -> Ap f tree -> Ap f tree
(¦) = liftA2 (¦)
instance (Biapplicative bi, Treey tree1, Treey tree2) => Treey (Biap bi tree1 tree2) where
leaf :: Int -> Biap bi tree1 tree2
leaf = liftA2 bipure leaf leaf
@Icelandjack
Icelandjack / showelem.hs
Last active September 17, 2020 22:31
instance pi n. Show (Fin n)
data SVec :: forall n a. Vec n a -> Type where
SVecO :: SVec VecO
SVecS :: Sing a -> SVec as -> SVec (a :> as)
type instance Sing @(Vec n a) = SVec @n @a
instance SingI VecO where
sing :: Sing VecO
sing = SVecO
@Icelandjack
Icelandjack / On.hs
Created January 13, 2020 12:13
singletons + On + via
{-# Language DataKinds #-}
{-# Language DerivingVia #-}
{-# Language FlexibleInstances #-}
{-# Language GADTs #-}
{-# Language InstanceSigs #-}
{-# Language PolyKinds #-}
{-# Language RankNTypes #-}
{-# Language ScopedTypeVariables #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeApplications #-}