| // Exercises from http://fsharpforfunandprofit.com/posts/computation-expressions-bind/ | |
| // Part 1 | |
| let strToInt str = | |
| match System.Int32.TryParse str with | |
| | (false, _) -> None | |
| | (true, x) -> Some x | |
| type YourWorkflowBuilder() = | |
| member this.Bind(x, f) = Option.bind f x |
| let preheatedOven = preheat oven 175<C> | |
| let preparedPans = map (grease >> flour) pans | |
| let flourMixture = whisk [ flour ; bakingSoda ; salt ] | |
| creamUntil (all [ light ; fluffy ]) [ butter ; whiteSugar ; brownSugar ] | |
| |> beatInOneAtATime eggs | |
| |> mix bananas | |
| |> addAlternately [ flourMixture ; buttermilk ] | |
| |> stir (walnuts |> chop) | |
| |> pourInto preparedPans | |
| |> bake preheatedOven 30<min> |
| module Tutorial where | |
| data Nat : Set where | |
| zero : Nat | |
| suc : Nat -> Nat | |
| {-# BUILTIN NATURAL Nat #-} | |
| infix 3 _+_ | |
| _+_ : Nat -> Nat -> Nat |
Writing Programs That Construct Proofs, Constable et al. 1984.
Beautiful introduction. Quite readable without much knowledge. Discusses λ-PRL. Defines tactics and tacticals.
Constructive Mathematics and Automatic Program Writers, Constable 1971
Lots of literature here
| ghc: panic! (the 'impossible' happened) | |
| (GHC version 7.10.2 for x86_64-apple-darwin): | |
| Simplifier ticks exhausted | |
| When trying UnfoldingDone $j_sdNBZ | |
| To increase the limit, use -fsimpl-tick-factor=N (default 100) | |
| If you need to do this, let GHC HQ know, and what factor you needed | |
| To see detailed counts use -ddump-simpl-stats | |
| Total ticks: 63261443 | |
| Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug |
| using System; | |
| using System.Collections.Generic; | |
| using System.Linq; | |
| using static System.Console; | |
| using static System.Math; | |
| using static Functional; | |
| public static class Functional | |
| { | |
| public static Func<X, Z> Compose<X, Y, Z>(Func<Y, Z> g, Func<X, Y> f) => x => g(f(x)); |
| module ResolveMaybe where | |
| data Maybe (A : Set) : Set where | |
| none : Maybe A | |
| some : A → Maybe A | |
| data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where | |
| refl : x ≡ x | |
| {-# BUILTIN EQUALITY _≡_ #-} | |
| {-# BUILTIN REFL refl #-} |
| module GreekScript3 where | |
| data Empty : Set where | |
| Not : Set → Set | |
| Not x = x → Empty | |
| data _And_ (A B : Set) : Set where | |
| _and_ : (a : A) → (b : B) → A And B |
Lambda Calculus
Church, Alonzo. The Calculi of Lambda Conversion. Princeton University Press, 1941.
Barendregt, Henk P. The Lambda Calculus. North Holland, revised edition, 1984.
Barendregt, Henk P. Functional programming and lambda calculus. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B, chapter 7, pages 321–364. Elsevier / MIT Press, 1990.
Hindley, J. Roger and Jonathan P. Seldin. Introduction to Combinators andλ-Calculus, volume 1 of London Mathematical Society Student Texts. Cambridge University Press, 1986.