Icelandjack

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

Icelandjack

Reddit discussion.

Disclaimer 1: Type classes are great but they are not the right tool for every job. Enjoy some balance and balance to your balance.

Disclaimer 2: I should tidy this up but probably won’t.

Disclaimer 3: Yeah called it, better to be realistic.

Type classes are a language of their own, this is an attempt to document features and give a name to them.

Icelandjack

wip, spin-off gists: https://gist.github.com/Icelandjack/e42495341f6029aad8c7e4e4a12c34ce

Monad gives Applicative, Applicative etc. gives Num, Floating, Fractional (regardless of actual subclass relationship)

Setting it up

WrapMonad tells us that a Monad implies Functor, Applicative

instance Monad m => Functor     (WrappedMonad m)

Icelandjack

import Data.Functor.Yoneda
import Data.Char
import Data.Kind

infixr 5
  ·

type  List :: (Type -> Type) -> Constraint
class List f where

Icelandjack

For the Trac ticket #14860.

All these types are valid for h, but its principal type involves -XQuantifiedConstraints

{-# Language FlexibleInstances, MultiParamTypeClasses, GADTs, QuantifiedConstraints #-}

import Data.Kind

type family FB (a::Type) (b::Type) :: Type where

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