Windows 64-bit 一鍵安裝包:http://www.cs.uiowa.edu/~astump/agda/ (備用連結(比較快)) 本安裝檔包含 GHC 7.8、Agda 2.4 以及 Emacs
- Haskell
ghc
與ghci
,GHC 提供的 Haskell 編譯器與交互式直譯器- 建議版本為 **GHC 7.8 (較舊版本例如 **7.6 也可以接受,而更新的版本 prelude 所提供的函數型別會與教學使用的有些落差)
- Agda
Windows 64-bit 一鍵安裝包:http://www.cs.uiowa.edu/~astump/agda/ (備用連結(比較快)) 本安裝檔包含 GHC 7.8、Agda 2.4 以及 Emacs
ghc
與 ghci
,GHC 提供的 Haskell 編譯器與交互式直譯器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 |
-- 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 |
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; |
{-# 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 node-gyp@3.4.0 | |
gyp info using node@8.9.3 | darwin | x64 | |
gyp verb command rebuild [] | |
gyp verb command clean [] |