Skip to content

Instantly share code, notes, and snippets.

Avatar

pasberth pasberth

View GitHub Profile
@pasberth
pasberth / a.md
Created Jun 21, 2015
ExistentialQuantification by Rank2Types
View a.md

存在型をλ式にエンコードする件について

Haskellには存在型というものがある。 これを使うとヘテロリストなどがつくれる例。

{-# LANGUAGE ExistentialQuantification  #-}
data T = forall t. Mk t
xs :: [T]
xs = [Mk 42, Mk "answer"]
View a.hs
-- ok
main :: IO ()
main = do
let x = Nothing
case x of
Just 0 -> return 0
Nothing -> return 1
case x of
Just "a" -> return 2
Nothing -> return 3
View a.v
Require Import Arith.
Goal forall n : nat, S (n + n + n * n) = S (n + n * S n).
Proof.
intro n.
rewrite <- mult_n_Sm.
rewrite <- plus_assoc.
rewrite (plus_comm n (n * n)).
reflexivity.
Qed.
@pasberth
pasberth / b.smi
Created Sep 28, 2014
SML# のオーバーロード
View b.smi
_require "basis.smi"
structure B =
struct
val g : int -> int
val h : string -> string
end
val f = case 'a in 'a -> 'a of
int => B.g
View README.md
ocamlfind ocamlc -package camlp4.extend,camlp4.quotations -syntax camlp4o -c pa_hello.ml
ocamlc -pp "camlp4o ./pa_hello.cmo" hello.ml
View README.md
$ ocamlfind ocamlc -syntax camlp4o -package js_of_ocaml.syntax -package lwt.syntax -package js_of_ocaml -package lwt -linkpkg a.ml
File "a.ml", line 1:
Error: Error while linking a.cmo:
Reference to undefined global `Lwt_main'
$ ocaml -version
The OCaml toplevel, version 4.01.0
$ opam list | grep -P 'js_of_ocaml|lwt'
js_of_ocaml             2.3  Compiler from OCaml bytecode to Javascript
lwt                   2.4.5  A cooperative threads library for OCaml
View hello.html
<html>
<head>
<title></title>
<script type="text/javascript" src="a.js"></script>
</head>
<body>
</body>
</html>
View README.md

ストラウストラップのプログラミング入門で登場する、

#include "std_lib_facilities.h"

という行は、すべて、次のプログラムに置き換えて 考えてください。

View a.js
function main(label) {
var i = 10;
GOTO:
while (true) {
switch (label) {
case "label1":
if (i == 0) {
console.log("ok!");
label = "label2";
continue GOTO;
View assign_self.cpp
#include <iostream>
struct A {
int x;
A(int x) : x(x) {}
void assign_self(A& a) {
*this = a;
}
};
You can’t perform that action at this time.