| let first p xs = | |
| let length = Array.length xs in | |
| (* mutable aray index *) | |
| let i = ref 0 in | |
| (* there are no loop breaks in OCaml anyway *) | |
| let break = ref false in | |
| while not (!break) && !i < length do | |
| if p (xs.(!i)) then break := true else i := (!i) + 1 | |
| done; | |
| !i |
| Intrinsically-typed de Bruijn representation of simply typed lambda calculus | |
| ============================================================================ | |
| \begin{code} | |
| open import Data.Nat | |
| open import Data.Empty | |
| hiding (⊥-elim) | |
| open import Relation.Nullary | |
| open import Relation.Binary.PropositionalEquality |
| // | |
| // Types | |
| // | |
| type t; | |
| type eventName = string; | |
| type listener('a) = 'a => unit; | |
| type listener2('a, 'b) = ('a, 'b) => unit; | |
| type listener3('a, 'b, 'c) = ('a, 'b, 'c) => unit; |
| -- This exercise covers the first 6 chapters of "Learn You a Haskell for Great Good!" | |
| -- Chapter 1 - http://learnyouahaskell.com/introduction | |
| -- Chapter 2 - http://learnyouahaskell.com/starting-out | |
| -- Chapter 3 - http://learnyouahaskell.com/types-and-typeclasses | |
| -- Chapter 4 - http://learnyouahaskell.com/syntax-in-functions | |
| -- Chapter 5 - http://learnyouahaskell.com/recursion | |
| -- Chapter 6 - http://learnyouahaskell.com/higher-order-functions | |
| -- Download this file and then type ":l Chapter-1-6.hs" in GHCi to load this exercise |
| {-# OPTIONS --without-K #-} | |
| module A where | |
| infixl 4 _≡_ | |
| data _≡_ {A : Set} (x : A) : A → Set where | |
| refl : x ≡ x | |
| J : (A : Set) (C : (x y : A) → x ≡ y → Set) | |
| → ((x : A) → C x x refl) |
CP is a process calculus presented by Philip Wadler in his paper "Propositions as sessions" (https://dl.acm.org/citation.cfm?id=2364568), as an attempt to bridge π-calculus with Linear logic.
Process calculus (like CP) provides a mean of modelling and describing the interactions and communications between a bunch of independent processes. The interaction between these processes are often described with some reduction rules.
| $ apm rebuild | |
| Rebuilding modules ✗ | |
| gyp info it worked if it ends with ok | |
| gyp verb cli [ '/Applications/Atom.app/Contents/Resources/app/apm/bin/node', | |
| gyp verb cli '/Applications/Atom.app/Contents/Resources/app/apm/node_modules/.bin/node-gyp', | |
| gyp verb cli 'rebuild' ] | |
| gyp info using [email protected] | |
| gyp info using [email protected] | darwin | x64 | |
| gyp verb command rebuild [] | |
| gyp verb command clean [] |
A monad is also a applicative functor, that seems pretty obvious, right?
Let's formalize this idea a bit:
This is record that houses the laws of applicative functors.
record IsApplicative {ℓ} (F : Set ℓ → Set ℓ)
(pure : {A : Set ℓ} → A → F A)
(_⊛_ : {A B : Set ℓ} → (F (A → B)) → F A → F B)
: Set (suc ℓ) where