lemastero

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

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

{-# 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

{-# 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)

lemastero

/** Showing with Kind-Polymorphism the evidence that Monad is a monoid in the category of endofunctors */
object Test extends App {

  /** Monoid (https://en.wikipedia.org/wiki/Monoid_(category_theory))
    * In category theory, a monoid (or monoid object) (M, μ, η) in a monoidal category (C, ⊗, I)
    * is an object M together with two morphisms
    *
    * μ: M ⊗ M → M called multiplication,
    * η: I → M called unit
    *

lemastero

import scalaz._, Scalaz._

// Adjunction between `F` and `G` means there is an
// isomorphism between `A => G[B]` and `F[A] => B`.
trait Adjunction[F[_],G[_]] {
  def leftAdjunct[A, B](a: A)(f: F[A] => B): G[B]
  def rightAdjunct[A, B](a: F[A])(f: A => G[B]): B
}

// Adjunction between free and forgetful functor.