puffnfresh

-- |
-- prop> \xs -> f (f xs) == xs
-- prop> \xs ys -> f ys ++ f xs == f (xs ++ ys)
f :: [a] -> [a]
f = foldl (flip (:)) []

puffnfresh

module Reverse where

open import Data.List as List hiding (reverse)
open import Data.List.Properties
open import Relation.Binary.PropositionalEquality

record ReverseLike (reverse : ∀ {A : Set} → List A → List A) : Set₁ where
  constructor rl
  field
    reverse0 : ∀ {A} → reverse {A} [] ≡ []

puffnfresh

Scala Lenz

This library is a port of Haskell's lens. The goal is to provide functional lenses, isomorphisms, getters and setters.

Examples

Isomorphisms

puffnfresh

function cabal_sandbox_info() {
    cabal_files=(*.cabal(N))
    if [ $#cabal_files -gt 0 ]; then
        if [ -f cabal.sandbox.config ]; then
            echo "%{$fg[green]%}sandboxed%{$reset_color%}"
        else
            echo "%{$fg[red]%}not sandboxed%{$reset_color%}"
        fi
    fi
}

puffnfresh

trait Wat[T]
object Wat {
  implicit object BooleanWat extends Wat[Boolean]
}

object Hello {
  implicit object AmbBooleanWat1 extends Wat[Boolean]
  implicit object AmbBooleanWat2 extends Wat[Boolean]

  def main(args: Array[String]) {

puffnfresh

import language.higherKinds

object Tagged {
  type @@[A, B] = { type T = A }

  type Id[A] = A

  implicit class Taggable[A](a: A) {
    def tagged[B]: A @@ B = a.asInstanceOf[A @@ B]
  }

puffnfresh

plusOne :: (Int -> Int) -> (Int -> Int)
plusOne = (. (+1))

timesTwo :: (Int -> Int) -> (Int -> Int)
timesTwo = (. (*2))

infixl 8 &

(&) :: a -> ((a -> a) -> (a -> a)) -> a
(&) = flip ($ id)

puffnfresh

import scalaz.{PLens, @?>}

// Ah, breaks the prism laws!

// > val two = within(_ == 2, PLens.plensId)
// > two.set(2, 3).flatMap(two.get)
// None

def within[A, B](f: A => Boolean, p: A @?> B): A @?> B = PLens.plens { (a: A) =>
  if (f(a))

puffnfresh

object Main extends SafeApp {
  def handleEvent(i: Int) =
    Task.delay {
      Task.fork(Task.delay {
        println(i)
        Thread.sleep(1000)
      }).runAsync(_ => ())
    }

  override def run(args: ImmutableArray[String]) = IO {

puffnfresh

// You won't be able to compile this with:

//    scala -language:dynamics NoDynamics.scala

// These two ambiguous implicits disable the `dynamics` feature.
implicit def ambDynamics1: language.dynamics.type = ???
implicit def ambDynamics2: language.dynamics.type = ???

object Woo extends Dynamic {
  def selectDynamic(name: String) = s"$name a mess of a language"