AndrasKovacs

Require Import Coq.Unicode.Utf8.

(*
As far as I can tell, there is way more literature in Agda on datatype-generic
programming than in Coq. I think part of the reason is that the Agda literature
makes liberal use of induction-recursion and fancy termination/positivity
checking, to define fixpoints of functors. These features are not available in
Coq.

claudio-naoto

@require: stdjabook
@require: code
@require: itemize
@require: tabular
@require: proof
@import: local

document (|
  title = {An outline of \SATySFi;};
  author = {Takashi SUWA};

linasm

sealed abstract class Perhaps[+A] {
  def foreach(f: A => Unit): Unit
  def map[B](f: A => B): Perhaps[B]
  def flatMap[B](f: A => Perhaps[B]): Perhaps[B]
  def withFilter(f: A => Boolean): Perhaps[A]
}

case class YesItIs[A](value: A) extends Perhaps[A] {
  override def foreach(f: A => Unit): Unit = f(value)
  override def map[B](f: A => B): Perhaps[B] = YesItIs(f(value))

johnhw

### JHW 2018
import numpy as np
import umap



# This code from the excellent module at:
# https://stackoverflow.com/questions/4643647/fast-prime-factorization-module
    
import random

Odomontois

package sb.church.lz

import ChOption._
import ChPair._
import ChBool._
import ChEither._
import ChList._
import Lambda._
import cats.Eval
import cats.syntax.apply._

djspiewak

Quick Tips for Fast Code on the JVM

I was talking to a coworker recently about general techniques that almost always form the core of any effort to write very fast, down-to-the-metal hot path code on the JVM, and they pointed out that there really isn't a particularly good place to go for this information. It occurred to me that, really, I had more or less picked up all of it by word of mouth and experience, and there just aren't any good reference sources on the topic. So… here's my word of mouth.

This is by no means a comprehensive gist. It's also important to understand that the techniques that I outline in here are not 100% absolute either. Performance on the JVM is an incredibly complicated subject, and while there are rules that almost always hold true, the "almost" remains very salient. Also, for many or even most applications, there will be other techniques that I'm not mentioning which will have a greater impact. JMH, Java Flight Recorder, and a good profiler are your very best friend! Mea

djspiewak

/*
 * Copyright 2017 Daniel Spiewak
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *     http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software

notxcain

import cats.data.{ EitherT, State }
import cats.implicits._
import cats.{ Monad, ~> }
import io.aecor.liberator.macros.free
import io.aecor.liberator.syntax._
import io.aecor.liberator.{ ProductKK, Term }

@free
trait Api[F[_]] {
  def doThing(aThing: String, params: Map[String, String]): F[Either[String, String]]

rubenpieters

//-------------------------
// Monad Transformer
//-------------------------

import cats.data._
import cats.implicits._
import cats._

type MonadStackStateTEither[ErrorType, StateType, ReturnType] =
StateT[Either[ErrorType, ?], StateType, ReturnType]

mandubian

/** 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
    *