View Product_of_Codes.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE DeriveGeneric #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE GeneralizedNewtypeDeriving #-} | |
{-# LANGUAGE InstanceSigs #-} | |
{-# LANGUAGE MultiParamTypeClasses #-} | |
{-# LANGUAGE PolyKinds #-} | |
{-# LANGUAGE ScopedTypeVariables #-} | |
{-# LANGUAGE StandaloneDeriving #-} | |
{-# LANGUAGE TypeApplications #-} |
View Applicative_Sum.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
View nary_composition.agda
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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) |
View Generics_Distr.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
View classless.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# Language EmptyCase #-} | |
{-# Language GADTs #-} | |
{-# Language InstanceSigs #-} | |
{-# Language PatternSynonyms #-} | |
{-# Language PolyKinds #-} | |
{-# Language ScopedTypeVariables #-} | |
{-# Language StandaloneKindSignatures #-} | |
{-# Language TypeApplications #-} | |
{-# Language TypeFamilies #-} | |
{-# Language TypeOperators #-} |
View Functor.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{- | |
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 |
View circ.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
View showelem.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
View On.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# Language DataKinds #-} | |
{-# Language DerivingVia #-} | |
{-# Language FlexibleInstances #-} | |
{-# Language GADTs #-} | |
{-# Language InstanceSigs #-} | |
{-# Language PolyKinds #-} | |
{-# Language RankNTypes #-} | |
{-# Language ScopedTypeVariables #-} | |
{-# Language StandaloneKindSignatures #-} | |
{-# Language TypeApplications #-} |
NewerOlder