lemastero

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

lemastero

{-# LANGUAGE RankNTypes, GADTs #-}
import Data.Functor.Adjunction

import Data.Functor.Identity
import Data.Functor.Product
import Data.Functor.Const


newtype Left f g = L (forall l. (f l -> g l) -> l)
cata :: (f a -> g a) -> Left f g -> a

lemastero

{-# LANGUAGE GADTs #-}
import Data.Functor.HCofree
import Data.Vec.Lazy
import Data.Fin
import Data.Type.Nat

data Cotra f a where
  Cotra :: SNat n -> f (Fin n) -> Vec n a -> Cotra f a

to :: Functor f => Cotra f a -> HCofree Traversable f a

lemastero

import scala.language.existentials

class A { class E }
class B extends A { class E }
trait CD { type E }
trait C extends CD { type E = Int }
trait D extends CD { type E = String }
 
object Test {
  type EE[+X <: { type E }] = X#E

lemastero

(* An initial attempt at universal algebra in Coq.
   Author: Andrej Bauer <Andrej.Bauer@andrej.com>

   If someone knows of a less painful way of doing this, please let me know.

   We would like to define the notion of an algebra with given operations satisfying given
   equations. For example, a group has of three operations (unit, multiplication, inverse)
   and five equations (associativity, unit left, unit right, inverse left, inverse right).
*)

lemastero

import scala.language.higherKinds

trait LeftContravariant[F[_,_]] {
  def contramap[A,AA,B](fa: F[A,B])(f: AA => A): F[AA,B]
}

trait RightCovariant[F[_,_]] {
  def map[A,B,BB](fa: F[A,B])(g: B => BB): F[A,BB]
}

lemastero

import Wizard.ConstUnit
import Wizard.Id

import scala.language.higherKinds

/*
Are there any constructions in Category Theory something like:

Given:
C category

lemastero

import scalaz.{Comonad, Monad}
import scalaz.{Arrow, Contravariant, Profunctor}
import scalaz.{Lan, Ran}

object AnyAndNothingInstances {

  // Monad
  // https://twitter.com/runarorama/status/1085383309969014784
  type FYea[A] = Any

lemastero

{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE StandaloneDeriving #-}

lemastero

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}   
                                                           
import Control.Applicative
import Data.Char
import Data.List (intersperse)
import Data.Monoid hiding (All, Any)
import Data.Foldable hiding (all, any)
import Prelude hiding (all, any)