pasberth pasberth

## a.md

      
              1 file
            
          
              0 forks
            
          
              0 comments
            
          
              0 stars
            
          
                pasberth
                / a.md
            
            
              Created
              June 21, 2015 18:05
            
              
                ExistentialQuantification by Rank2Types
              
          
    存在型をλ式にエンコードする件について

Haskellには存在型というものがある。
これを使うとヘテロリストなどがつくれる例。
{-# LANGUAGE ExistentialQuantification  #-}
data T = forall t. Mk t
xs :: [T]
xs = [Mk 42, Mk "answer"]

  
## 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

## 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.

## 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

## README.md

      
              3 files
            
          
              0 forks
            
          
              0 comments
            
          
              0 stars
            
          
                pasberth
                / README.md
            
            
              Created
              August 14, 2014 05:31
            
          
    ocamlfind ocamlc -package camlp4.extend,camlp4.quotations -syntax camlp4o -c pa_hello.ml
ocamlc -pp "camlp4o ./pa_hello.cmo" hello.ml


## README.md

      
              2 files
            
          
              0 forks
            
          
              0 comments
            
          
              0 stars
            
          
                pasberth
                / README.md
            
            
              Last active
              August 29, 2015 14:04
            
          
    $ 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


## hello.html
<html>
<head>
  <title></title>
  <script type="text/javascript" src="a.js"></script>
</head>
<body>

</body>
</html>

## README.md

      
              4 files
            
          
              0 forks
            
          
              0 comments
            
          
              0 stars
            
          
                pasberth
                / README.md
            
            
              Last active
              August 29, 2015 14:02
            
          
    ストラウストラップのプログラミング入門で登場する、
#include "std_lib_facilities.h"
という行は、すべて、次のプログラムに置き換えて
考えてください。


## 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;

## assign_self.cpp
#include <iostream>

struct A {
  int x;
  A(int x) : x(x) {}
  void assign_self(A& a) {
    *this = a;
  }
};
	-- 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
	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.
	_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
	<html>
	<head>
	<title></title>
	<script type="text/javascript" src="a.js"></script>
	</head>
	<body>

	</body>
	</html>
	function main(label) {
	var i = 10;
	GOTO:
	while (true) {
	switch (label) {
	case "label1":
	if (i == 0) {
	console.log("ok!");
	label = "label2";
	continue GOTO;
	#include <iostream>

	struct A {
	int x;
	A(int x) : x(x) {}
	void assign_self(A& a) {
	*this = a;
	}
	};