sjoerdvisscher

{-# LANGUAGE RankNTypes, GADTs, TypeOperators #-}
import Data.Profunctor

data Exists2 f g where
  Exists2 :: f x -> g x -> Exists2 f g

data Confluence p = Confluence (forall a b c. (p a b, p a c) -> Exists2 (p b) (p c))

newtype Op p a b = Op { runOp :: p b a }

sjoerdvisscher

{-# LANGUAGE TypeOperators, RankNTypes, TupleSections, GADTs, DeriveFunctor, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, TypeFamilies, AllowAmbiguousTypes, TypeApplications, ScopedTypeVariables, UndecidableInstances #-}

import Data.Bifunctor
import Data.Functor.Kan.Lan
import Data.Kind (Type)
import Data.Void (Void, absurd)

type f ~> g = forall a. f a -> g a

class Bifunctor m => Tensor m where

sjoerdvisscher

{-# LANGUAGE GHC2021, GADTs, DataKinds #-}
module Endofunctors where

import Control.Comonad (Comonad(..))
import Control.Comonad.Cofree (Cofree(..))
import Control.Monad (join, ap, void)
import Control.Monad.Free (Free(..))
import Data.Bifunctor (first, second, bimap)
import Data.Functor.Day
import GHC.Generics

sjoerdvisscher

{-# LANGUAGE ConstraintKinds, TypeApplications, ScopedTypeVariables, FlexibleInstances, RankNTypes, DeriveFunctor #-}
import Data.Functor.Compose
import Data.Functor.Identity

class Cofunctor f where
  comap :: (f a -> f b) -> (a -> b)

instance Cofunctor Identity where
  comap f = runIdentity . f . Identity

sjoerdvisscher

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE TypeOperators #-}
module StateMachine where

import Control.Comonad (extract)
import Control.Comonad.Cofree
import Data.Bifunctor (first, second)
import Data.Functor.Day

sjoerdvisscher

{-# LANGUAGE TypeOperators, FlexibleContexts #-}
import GHC.Generics ((:.:)(..))
import Control.Applicative (liftA2)

class Applicative f => Selective f where
  select :: f (Either a b) -> f (a -> b) -> f b
  select fe fab = either id (uncurry (flip ($))) <$> biselect (either Right Left <$> fe) (Right <$> fab)
  biselect :: f (Either a b) -> f (Either a c) -> f (Either a (b, c))

class Applicative f => CheckClosed f where

sjoerdvisscher

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}

import Data.Kind (Type)

sjoerdvisscher

{-# LANGUAGE GHC2021, PatternSynonyms, LambdaCase, DataKinds, PolyKinds, TypeFamilies, NoStarIsType, UndecidableInstances, UndecidableSuperClasses, AllowAmbiguousTypes, DefaultSignatures #-}

import Data.Functor (void)
import Data.Bifunctor (bimap)
import Data.Kind (Type, Constraint)
import Data.Void
-- from fin
import Data.Fin (Fin(..))
import qualified Data.Fin as Fin
import Data.Type.Nat

sjoerdvisscher

-- https://icfp21.sigplan.org/details/icfp-2021-papers/21/Calculating-Dependently-Typed-Compilers-Functional-Pearl-
{-# LANGUAGE GADTs, DataKinds, TypeOperators, TypeFamilies, TypeApplications, KindSignatures, ScopedTypeVariables #-}
import Control.Applicative
import Data.Kind
import Data.Type.Equality

type family (a :: Bool) || (b :: Bool) :: Bool where
  'False || b = b
  'True || b = 'True

sjoerdvisscher

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}