Skip to content

Instantly share code, notes, and snippets.

View lemastero's full-sized avatar
🕺
Everything is possible!

Piotr Paradziński lemastero

🕺
Everything is possible!
View GitHub Profile
@lemastero
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 _⊕_
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
lemastero / ProfunctorOptics.scala
Last active August 28, 2020 00:02
Profunctor Optics in Scala
import scala.language.higherKinds
/*
Mainline Profunctor Heirarchy for Optics: https://r6research.livejournal.com/27476.html
Profunctor Optics: The Categorical Approach - Bartosz Milewski: https://www.youtube.com/watch?v=l1FCXUi6Vlw
*/
object ProfunctorOpticsSimpleImpl {
trait Functor[F[_]] {
def map[A, B](x: F[A])(f: A => B): F[B]
@lemastero
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
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
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
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
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 <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
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
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