wenkokke

Tactics in Agda

This gist is my attempt to list all projects providing proof automation for Agda.

Glossary

When I say tactic, I mean something that uses Agda's reflection to provide a smooth user experience, such as the solveZ3 tactic from Schmitty:

_ : ∀ (x y : ℤ) → x ≤ y → y ≤ x → x ≡ y
_ = solveZ3

DanBurton

#!/usr/bin/env stack
{- stack
  script
  --resolver lts-11.16
  --package bytestring
  --package http-conduit
-}

-- usage: ./Main.hs
-- modify the baseUrl and ghcDateVersion to taste

graninas

Software Transactional Memory in C++: pure functional approach (Tutorial)

In this article I’ll tell you about my pure functional library for Software Transactional Memory (STM) that I’ve built in C++. I adopted some advanced functional programming concepts that make it composable and convenient to use. Its implementation is rather small and robust, which differentiates the library from competitors. Let’s discuss what STM is and how to use it.

• Intro
• Links
• Software Transactional Memory
• STM basics
• Composable transactions
• Dining Philosophers: The task

sellout

-- | A “flushing” 'stream', with an additional coalgebra for flushing the
--   remaining values after the input has been consumed. This also allows us to
--   generalize the output away from lists.
fstream
  :: (Cursive t (XNor a), Cursive u f, Corecursive u f, Traversable f)
  => Coalgebra f b -> (b -> a -> b) -> Coalgebra f b -> b -> t -> u
fstream ψ g ψ' = go
  where
    go c x = 
      let fb = ψ c

mstksg

{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE UndecidableInstances #-}

import           Data.Proxy
import           Data.Reflection

data EqDict a = EQD { withEqDict :: a -> a -> Bool }

ChrisPenner

const all = (...preds) => (obj) => preds.map(f => f(obj)).reduce((a, b) => a && b, true)
const any = (...preds) => (obj) => preds.map(f => f(obj)).reduce((a, b) => a || b, false)
const oneOf = (...preds) => (obj) => preds.map(f => f(obj)).reduce((a, b) => a ? !b : b, false)
const has = (prop) => (obj) => obj[prop] !== undefined
const not = (pred) => (obj) => !pred(obj)
const equals = (prop, val) => (obj) => obj[prop] === val
const implies = (f, g) => (obj) => !f(obj) || g(obj);

const validate = all(implies(has('selectedIndex'), equals('isOpen', true)))

busypeoples

SetState React HigherOrderComponent

Why?

If you want to write stateless functions in React and need to combine a number of setState functions to that stateless function. Enables to compose a number of functions expecting state and props. This enables to reuse functions when needed and eases testing those functions (as they are standalone and decoupled from React.

Example

phadej

title	author
Glassery	Oleg Grenrus

After I have improved the raw performance of optika – a JavaScript optics library, it's time to make the library (feature-)complete and sound. Gathering and classifying all possible optic types, gives us a reference point

mtesseract

The Problem

Defining records in Haskell causes accessor functions for the record's fields to be defined. There is no seperate namespace for these accessor functions.

The Goal

Be able to

• use records in Haskell, which share field names.
• use lenses for accessing these fields

michaelt

{-#LANGUAGE GADTs, TypeApplications, DataKinds, TypeOperators #-}
import Control.Monad.Freer
import qualified Control.Monad.Freer as F
import Control.Monad.Trans.Writer
import Control.Monad.IO.Class
type Loc = Int
type LogSource = Int
type LogLevel = Int
type LogStr = String