This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import os | |
""" | |
0: 1: 2: 3: 4: | |
aaaa .... aaaa aaaa .... | |
b c . c . c . c b c | |
b c . c . c . c b c | |
.... .... dddd dddd dddd | |
e f . f e . . f . f |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module SimpleEval where | |
import Prelude hiding (odd, even) | |
import Data.Dynamic | |
data Expr = Val Int | Add Expr Expr | |
data Cont = HALT | EVAL Expr Cont | ADD Int Cont | |
eval :: Expr -> Int |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#lang lazy | |
(define g | |
(lambda (f) | |
(lambda (n) | |
(if (= n 0) | |
1 | |
(* n (f (- n 1))))))) | |
(define f |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#lang lazy | |
(define g | |
(lambda (f) | |
(lambda (n) | |
(if (= n 0) | |
1 | |
(* n (f (- n 1))))))) | |
(define f |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Can where | |
import Relation.Binary.PropositionalEquality as Eq | |
import Data.Nat.Properties as Pro | |
open Pro using (+-assoc; +-identityʳ; +-suc; +-comm) | |
open Eq using (_≡_; refl; cong; sym) | |
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎) | |
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _^_) | |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#lang racket | |
;;(define Y | |
;; (lambda (f) | |
;; ((lambda (x) (f (x x))) (lambda (x) (f (x x)))) )) | |
;;(define almost-Y | |
;; (lambda (f) | |
;; ((lambda (x) (f (x x))) (lambda (x) (f (x x)))) )) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#lang racket | |
(define identity (lambda (x) x)) | |
(define (part-factorial0 self n) | |
(if (= n 0) | |
1 | |
(* n (self self (- n 1))))) ;; note the extra "self" here the same as below | |
(part-factorial0 part-factorial0 5) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#lang racket | |
;(Y f) = fixpoint-of-f | |
;(f fixpoint-of-f) = fixpoint-of-f | |
;(Y f) = fixpoint-of-f = (f fixpoint-of-f) | |
;(Y f) = (f (Y f)) | |
(define (Y f) (f (Y f))) | |
(define Y-lambda |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#lang racket | |
(define (factorial n) | |
(if (= n 0) | |
1 | |
(* n (factorial (- n 1))))) | |
(define factorial_lambda | |
(lambda (n) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE RebindableSyntax #-} | |
module Cartesian_product3 where | |
import Prelude hiding((>>=), return, Monad, fail) | |
-- begin help ----- | |
class Applicative m => Monad m where | |
return :: a -> m a |
NewerOlder