View ProfunctorOpticsCategoricalUpdate.hs
{-# LANGUAGE AllowAmbiguousTypes #-} | |
{-# LANGUAGE ConstraintKinds #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE GADTs #-} | |
{-# LANGUAGE MultiParamTypeClasses #-} | |
{-# LANGUAGE QuantifiedConstraints #-} | |
{-# LANGUAGE RankNTypes #-} | |
{-# LANGUAGE ScopedTypeVariables #-} | |
{-# LANGUAGE TypeApplications #-} | |
{-# LANGUAGE TypeOperators #-} |
View haginoGen.hs
{-# 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 |
View Cotra.hs
{-# 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 |
View Unsoundness.scala
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 |
View algebra.v
(* 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). | |
*) |
View ProfunctorBifunctorHierarchy.scala
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] | |
} |
View ModularCategoryTheory.scala
import Wizard.ConstUnit | |
import Wizard.Id | |
import scala.language.higherKinds | |
/* | |
Are there any constructions in Category Theory something like: | |
Given: | |
C category |
View WordsAboutNothingAndAny.scala
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 |
View ttg.hs
{-# OPTIONS_GHC -Wall #-} | |
{-# LANGUAGE TypeFamilies #-} | |
{-# LANGUAGE PatternSynonyms #-} | |
{-# LANGUAGE BangPatterns #-} | |
{-# LANGUAGE LambdaCase #-} | |
{-# LANGUAGE MultiParamTypeClasses #-} | |
{-# LANGUAGE FunctionalDependencies #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE UndecidableInstances #-} | |
{-# LANGUAGE StandaloneDeriving #-} |
View Sudoku.hs
{-# 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) |
NewerOlder