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

Icelandjack

-- SYSTEM F
--   http://homepages.inf.ed.ac.uk/slindley/papers/embedding-f.pdf
-- 
-- Type-level lambdas
--   https://gist.github.com/AndrasKovacs/ac71371d0ca6e0995541e42cd3a3b0cf


{-# language TemplateHaskell, ScopedTypeVariables, RankNTypes,
             TypeFamilies, UndecidableInstances, DeriveFunctor, GADTs,
             TypeOperators, TypeApplications, AllowAmbiguousTypes,

Icelandjack

Solving Trac ticket #14832:

{-# Language QuantifiedConstraints, ScopedTypeVariables, TypeOperators, GADTs, FlexibleInstances, UndecidableInstances, ConstraintKinds, MultiParamTypeClasses, InstanceSigs, TypeApplications #-}

import Prelude hiding (id, (.))
import Control.Category
import Data.Coerce

data Dict c where