Skip to content

Instantly share code, notes, and snippets.

@Icelandjack
Icelandjack / Product_of_Codes.hs
Created Jul 30, 2022
Implement product of datatypes in generics-sop: liftA2 (++) of codes
View Product_of_Codes.hs
-- 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]]
--
View Applicative.hs
{-# 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 Oct 16, 2021
Deriving Applicative for sums of functors
View Applicative_Sum.hs
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 Oct 11, 2021
Dependent polyvariadic mixfix function composition in Agda
View nary_composition.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 Aug 13, 2021
Simplify and Distribute GHC.Generics
View Generics_Distr.hs
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 Jul 13, 2021
Classless GHC.Generics with Type.Reflection
View classless.hs
{-# Language EmptyCase #-}
{-# Language GADTs #-}
{-# Language InstanceSigs #-}
{-# Language PatternSynonyms #-}
{-# Language PolyKinds #-}
{-# Language ScopedTypeVariables #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeApplications #-}
{-# Language TypeFamilies #-}
{-# Language TypeOperators #-}
View Functor.hs
{-
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 Oct 3, 2020
Tree instance for Ap and Biap
View circ.hs
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 Sep 17, 2020
instance pi n. Show (Fin n)
View showelem.hs
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 Jan 13, 2020
singletons + On + via
View On.hs
{-# Language DataKinds #-}
{-# Language DerivingVia #-}
{-# Language FlexibleInstances #-}
{-# Language GADTs #-}
{-# Language InstanceSigs #-}
{-# Language PolyKinds #-}
{-# Language RankNTypes #-}
{-# Language ScopedTypeVariables #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeApplications #-}