Piotr Paradziński lemastero

🕺

Everything is possible!

Apply formal methods, category theory, type theory to build: blockchains / compilers / big data in Scala / Haskell / Idris / Agda @ScalaConsultants

lemastero / Queue.agda

Created September 1, 2021 23:23 — forked from andrejbauer/Queue.agda

An implementation of infinite queues fashioned after the von Neuman ordinals

	open import Data.Nat
	open import Data.Maybe
	open import Data.Product

	-- An implementation of infinite queues fashioned after the von Neuman ordinals

	module Queue where

	infixl 5 _⊕_

lemastero / InferenceMatchablePlugin.scala

Created July 6, 2021 08:22 — forked from xuwei-k/InferenceMatchablePlugin.scala

	import dotty.tools.dotc.ast.tpd.TypeTree
	import dotty.tools.dotc.core.Contexts.Context
	import dotty.tools.dotc.core.Symbols.defn
	import dotty.tools.dotc.plugins.{PluginPhase, StandardPlugin}
	import dotty.tools.dotc.typer.FrontEnd
	import dotty.tools.dotc.report

	class InferenceMatchablePlugin extends StandardPlugin {
	override def name = "inference-matchable-plugin"

lemastero / ProfunctorOpticsCategoricalUpdate.hs

Created January 26, 2020 23:19

Profunctor optics, a categorical update - Bryce Clarke, Derek Elkins, Jeremy Gibbons, Fosco Loregian, Bartosz Milewski, Emily Pillmore, Mario Román

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

lemastero / haginoGen.hs

Created December 9, 2019 01:58 — forked from sjoerdvisscher/haginoGen.hs

Categorical Data Types ala Hagino in 2 different ways

	{-# 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 / Cotra.hs

Created November 28, 2019 20:51 — forked from sjoerdvisscher/Cotra.hs

Cofree traversable functor

	{-# 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 / Unsoundness.scala

Created November 28, 2019 09:27 — forked from sir-wabbit/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

lemastero / algebra.v

Created October 5, 2019 19:58 — forked from andrejbauer/algebra.v

Uinversal algebra in Coq

	(* An initial attempt at universal algebra in Coq.
	Author: Andrej Bauer <[email protected]>

	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 / ProfunctorBifunctorHierarchy.scala

Created May 13, 2019 23:57

Profunctor and Bifunctor can be expressed using 3 more basic abstractions. This nicely split organise laws for them.

	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 / ModularCategoryTheory.scala

Created May 13, 2019 23:21

Modular approach to abstractions from Category Theory

	import Wizard.ConstUnit
	import Wizard.Id

	import scala.language.higherKinds

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

	Given:
	C category

lemastero / WordsAboutNothingAndAny.scala

Last active January 28, 2019 23:47

What we say when we say F.. Yea! or F... No!

	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