Icelandjack

newtype (f `RepVia` via) a = RepVia (f a)

instance (Representable f, Coercible via (Rep f)) => Functor (f `RepVia` via) where
 fmap :: forall a b. (a -> b) -> ((f `RepVia` via) a -> (f `RepVia` via) b)
 fmap = coerce $ fmapRep @f @a @b

instance (Representable f, Coercible via (Rep f)) => Distributive (f `RepVia` via) where
 collect :: forall g a b. Functor g => (a -> (f `RepVia` via) b) -> (g a -> (f `RepVia` via) (g b))
 collect = coerce (collect @f @g @a @b)

Icelandjack

{-# Language DeriveFunctor              #-}
{-# Language DerivingVia                #-}
{-# Language FlexibleContexts           #-}
{-# Language FlexibleInstances          #-}
{-# Language GADTs                      #-}
{-# Language GeneralizedNewtypeDeriving #-}
{-# Language InstanceSigs               #-}
{-# Language ScopedTypeVariables        #-}
{-# Language TypeApplications           #-}
{-# Language TypeFamilies               #-}

Icelandjack

-- https://www.reddit.com/r/haskell/comments/abxem5/experimenting_with_kleisli_instance_of/

{-# Language TypeApplications     #-}
{-# Language RankNTypes           #-}
{-# Language DataKinds            #-}
{-# Language KindSignatures       #-}
{-# Language PolyKinds            #-}
{-# Language TypeOperators        #-}
{-# Language GADTs                #-}
{-# Language TypeFamilies         #-}

Icelandjack

I was implementing "variable-arity zipWith" from Richard Eisenberg's thesis (recommended) when I noticed it used

apply :: [a -> b] -> [a] -> [b]
apply (f:fs) (a:as) = f a : apply fs as
apply _      _      = []

and

repeat :: a -> [a]

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

{-# Language RankNTypes              #-}
{-# Language LambdaCase              #-}
{-# Language TypeOperators           #-}
{-# Language TypeApplications        #-}
{-# Language PolyKinds               #-}
{-# Language TypeFamilies            #-}
{-# Language FlexibleInstances       #-}
{-# Language GADTs                   #-}
{-# Language ConstraintKinds         #-}
{-# Language MultiParamTypeClasses   #-}

Icelandjack

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

infixr 5
  ·

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

Icelandjack

data Kl_kind :: (Type -> Type) -> Type where
  Kl :: Type -> Kl_kind(m)
  
type family
  UnKl (kl :: Kl_kind m) = (res :: Type) | res m -> kl where
  UnKl (Kl a) = a

Icelandjack

Non-standard operators I use :) linked to from my twitter profile

I use kind synonyms

type T   = Type
type TT  = T -> T
type TTT = T -> TT
type C   = Constraint
type TC  = T -> C

Icelandjack

-- type Sig k = [k] -> Type
-- 
-- data AST :: Sig k -> Sig k where
--   Sym  :: dom a -> AST dom a
--   (:$) :: AST dom (a:as) -> AST dom '[a] -> AST dom as

singletons [d| data N = O | S N |]

infixr 5 :·
data Vec :: N -> Type -> Type where