Icelandjack

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

{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs               #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE PolyKinds                  #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE TypeApplications           #-}

Icelandjack

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

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

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

{-# Language EmptyCase                #-}
{-# Language GADTs                    #-}
{-# Language InstanceSigs             #-}
{-# Language PatternSynonyms          #-}
{-# Language PolyKinds                #-}
{-# Language ScopedTypeVariables      #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeApplications         #-}
{-# Language TypeFamilies             #-}
{-# Language TypeOperators            #-}

Icelandjack

{-
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

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

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

{-# Language DataKinds                #-}
{-# Language DerivingVia              #-}
{-# Language FlexibleInstances        #-}
{-# Language GADTs                    #-}
{-# Language InstanceSigs             #-}
{-# Language PolyKinds                #-}
{-# Language RankNTypes               #-}
{-# Language ScopedTypeVariables      #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeApplications         #-}