読者です 読者をやめる 読者になる 読者になる

こわくない Idris (6)

表明から証明へ (3) headを証明する HaskellのPrelude.headとは異なり、IdrisのPrelude.List.headは、引数にコンスセルである証明をとるので、全域函数になっている。Idrisのシステムでは次のように、%assert_total宣言によって、全域函数であることが「表明…

こわくない Idris (5)

表明から証明へ (2) 型と命題 カリー゠ハワード同型対応により、プログラムと証明が対応すると述べた。実際にはどのように対応しているのだろうか? 実は、恒真である命題は、空でない(その型である値を持つ)型に対応しているのだ。 型と命題の対応関係を見…

こわくない Idris (4)

表明から証明へ 表明とテスト バグの原因のひとつとして、プログラム実行時に守るべき条件が守られていないことが挙げられるだろう。プログラムが一体どのような場合に正常に動作し、どのような場合に望まない結果をもたらすのかが分かっていなければ、バグ…

こわくない Idris (3)

ハロー、依存型プログラミングの世界 (3) 依存ペア 依存ペア dependent pair とは、ある値と、その値に依存した型を持つ値のペアのことだ。 data Exists : (a : Type) -> (P : a -> Type) -> Type where Ex_intro : {P : a -> Type} -> (x : a) -> P x -> Ex…

こわくない Idris (2)

ハロー、依存型プログラミングの世界 (2) データ型の宣言 代数データ型を宣言する場合には、Haskellと同様の記法を使うことができる。HaskellでもおなじみのEitherやListの宣言はidrisではこうなっている。 data Either a b = Left a | Right b data List a …

こわくない Idris (1)

はじめに Idrisという、Haskellに似ていて、依存型 dependent type を持っている言語がある。依存型を持った言語なんて他にもあるのだけれども、Idrisは general purpose を謳っている。わざわざ汎用って謳っているあたり、依存型ってのはもっと色々に使える…

haxe.Utf8の非互換性

次のコードの出力を各プラットフォームで比較する。(現時点のGitHub上にある開発版を使う。) import haxe.Utf8; class Hello { public static function main() { trace("あ𠀀い"); trace("あ𠀀い".length); trace("あ𠀀い".charCodeAt(1)); trace("あ𠀀い".c…

Rust 0.7

前回: Rust 0.4 - M59のブログRust 0.7 向けに書きなおし。 // for Rust 0.7 extern mod extra; use sort = extra::sort::quick_sort; fn main() { let (port, chan) = stream(); let chan = std::comm::SharedChan::new(chan); for std::uint::iterate(0, 1…

Pixilang マニュアル (英語) PixilangV3Manual - pixilang - Simple programming language for small graphics/sound applications and experiments - Google Project Hosting

ピクセル指向プログラミング言語 Pixilang (3)

アニメーション グラフィックスを動かしてみる。 while 1 { t_rotate( 1, 0, 0, 1 ) clear() dot( 0, 0, WHITE ) line( 0, 100, 100, 0, ORANGE ) box( -100, -100, 50, 100, RED ) fbox( 100, -100, 100, 50, #ffeecc ) frame() while get_event() { if EVT…

ピクセル指向プログラミング言語 Pixilang (2)

Pixilang入門の下書きみたいなものだと思ってください。 エラー プログラムに間違いがあると、エラーになることがある。 たとえば、次のプログラム while 1 { print( "Hello, world! ) frame() while get_event() { if EVT[ EVT_TYPE ] == EVT_QUIT { halt }…

ピクセル指向プログラミング言語 Pixilang

Pixilangは、小規模なグラフィックス・サウンドアプリの作成や試作に向いた「ピクセル指向」プログライング言語だ。処理系がMIT Licenseのもとで公開されている。グラフィックスやサウンド処理に便利な機能が最初から用意されているし、しかもクロスプラット…

函数論理プログラミング言語 Curry

Curryはfunctional logic programming languageという聞きなれないカテゴリーに属する言語だ。もっとも、函数型プログラミングと論理型プログラミングは似通った点もあるから、そのふたつのパラダイムを併せ持ったプログラミング言語が存在するのはそんなに…

LibreLogoを使う

Ubuntu 13.04 (Raring Ringtail) で入る LibreOffice 4.0 には、ロゴで図形を描画する機能がある。 Raring リポジトリから必要なパッケージをインストールする。 $ sudo apt-get install libreoffice-script-provider-python libreoffice-librelogoそしてLib…

プログラミング言語 Proxima

id ::= \x -> x pred ::= succ \x -> x Nat ::= zero | succ Nat nat \z \s ::= zero -> z | succ \n -> s (nat z s n) Nat + Nat :: Nat \x + \y = nat x succ y Nat - Nat :: Nat \x - \y = nat x (pred | id) y

asm.js is 何

解説記事じゃないですし、内容は保証しません。 asm.js は低レベル言語 仕様書[1]によれば、asm.jsはJavaScriptの厳密なサブセットであって、コンパイラーの低レベルで効率的なターゲット言語として使うことができる言語だ。 This specification defines asm…

3DCGスクリプト言語案 save obj > "alpha.obj" let $cube = load obj < "cube.obj" for $r1 $r2 in load csv < "value.tsv" begin translate 5 0 0 rotate $r1 0 0 1 model $cube end begin translate -5 0 0 rotate $r2 0 0 1 model $cube end

ラムダ++

#include <iostream> int main() { for (int i = 0; i < 10; ++i) { auto x = [=](){ return i; }; std::cout << x() << std::endl; } } prog_cpp$ g++ -std=c++0x hellolambda.cpp prog_cpp$ ./a.out 0 1 2 3 4 5 6 7 8 9 prog_cpp$</iostream>

ラムダラムダ

TypeScriptは ()=> で Java8は ()-> なのか。辛い。2013-03-12 13:58:59 via SoraUsagi C++ [](int x) { return x > 0; } Python lambda x: x > 0 Ruby -> x { x > 0 } Haskell \x -> x > 0 C# x => x > 0 CoffeeScript (x) -> x > 0

Bool ::= False | True Nat ::= O | S Nat Maybe a ::= Nothing | Just a Not :: Bool -> Bool Not = False -> True | True -> False Match :: _ -> _ -> Bool Match a = a -> True | _ -> False Pred ::= S (x : Nat) -> x

send more money

import Control.Monad import Control.Applicative digit :: MonadPlus m => m Int digit = msum $ map return [0..9] exps :: Num a => [a] exps = map (10 ^) [0..] number :: Num a => [a] -> a number = sum . zipWith (*) exps . reverse uniqueDigits …

blockly - A visual programming editor - Google Project Hosting ..::CLAM::.. C++ Library for Audio and Music

もっと色々なプログラミング言語を調べて比較してみよう

項書き換えに基づく関数型プログラミング言語 Pure

Pure Programming Language デフォルトは正格評価。指定すれば遅延評価も使える。 副作用を許容する。 バックエンドにLLVMを使っている。 C FFIを持つ。C言語などで書かれたライブラリを、簡単な宣言で呼び出すことができる。 変数には型がないが、データの…

プログラミングパラダイムについて何か書こうと思ったけど挫折。

できていないパーサーの作り直し。演算子の数を増やす。関数型言語のように、自由に定義できるようにする。

名前の話(仮)

名前の管理はプログラミングにおいて大きな問題だ。名前は恣意的に付けることができるが、異なるものには異なる名前を付けないといけない。限られた名前を管理して、名前の衝突を避けなければならない。しかしあらゆるものを固有名で呼ぶこともできないから…

module Free data Free : (Type -> Type) -> Type -> Type where Pure : a -> Free f a Impure : f (Free f a) -> Free f a bind : Functor f => (a -> Free f b) -> Free f a -> Free f b bind k (Pure x) = k x bind k (Impure x) = Impure (fmap (bind k)…

CoffeeScriptで遅延評価(もどき)を実装しよう

遅延評価をまねる 厳密に言えば、遅延評価は式の評価戦略 evaluation strategy のひとつだ。JavaScriptとかLuaは正格な評価を行い、Haskellは非正格な評価を行う。正格な言語で非正格評価を真似る方法のひとつに、引数をすべてクロージャーでくるみ、使うと…

Coq 帰納法と余帰納法

前回、iterateとtakeを定義した。 Require Import List. Require Import Coq.Lists.Streams. Section MyStreams. Variable A : Type. CoFixpoint iterate (f : A -> A) (x : A) : Stream A := Cons x (iterate f (f x)). Fixpoint take (n : nat) (s : Strea…

ビジュアルプログラミング言語作りたい。色々調べる。ビジュアルプログラミング言語 - Wikipediaデータフロープログラミング - WikipediaLucid (プログラミング言語) - Wikipedia 1976年 「非ノイマン型 プログラミング言語の実験の為に設計された。」

無限リストと証明じゃないCoqの話

Haskellではじめて無限リストのコードを見たときはとても驚いた。遅延評価など知らないから、どうみても無限ループに陥りそうなプログラムがちゃんと動いているのが不思議だった。無限に続くデータさえ表現できる遅延データ構造はとても強力だ。大量のデータ…

融合変換の勉強しないとなー

遅延リストで素数

Prime numbers - HaskellWiki から移植。 -- from www.haskell.org/haskellwiki/Prime_numbers minus = (X, Y) -> return X if Y\empty! x, xs = X\head!, X\tail! y, ys = Y\head!, Y\tail! if x < y Sequence\ConsDelay (-> x), Delay -> minus xs, Y else…

Lua/MoonScriptで部分関数

昨日の続き。 util = require 'util' import Function, Switch, Case, Delay, List, Array, Sequence from util _ = util.it require 'std' print '# Function combination' print "(_ + 5 .. _ * 2)(1) ==> #{(_ + 5 .. _ * 2)(1)}" print '# Partial funct…

Lua/MoonScriptで遅延リスト

MoonScriptで遅延リストを実装した。 list = require 'list' import Function, Delay, List, Array, Sequence from list require 'std' local fib fib = Sequence\Table({1, 1})\appendDelay -> fib\zipWith op['+'], fib\tail! nat = Sequence\iterate (=> …

何でも無限リスト

純Lispにはアトムとリストがあるけど、アトムを無くして、なんでも無限リストにしたらどうだろう? 今までアトムだと思っていたものは、実はリストだったのだ。 なんでもリストだから、carとcdrは何にでも適用できる。carは左のリストを取り出し、cdrは右の…

新しいプログラミング言語

新言語登場 新しいプログラミング言語を作っています。mandel59/psil · GitHub現状はこんな感じ。 let x: 'ハロー' y: add(+'1', +'9') z: {a: x; b: y} debug.print "\(z.a)ワールド \(z.b)"……でも内容はこれから色々変えるので、多分このままの形では残り…

プログラミング言語Egisonのパターンマッチ機能をLua上で実装してみた

Programming Language Egison プログラミング言語Egisonは、強力なパターンマッチ機能を持つという。とりあえず、同じような機能をLua上で使えるように、MoonScriptを使って実装してみた。 mandel59/egimoon · GitHub print show match_all {1, 2, 3}, (List…

ぼくのかんがえた、さいきょうのげんご 1

周りで言語を考えたり処理系作ったりしている人がいると、自分でも作りたくなってきた。ここで、「僕の考えた最強の言語」の青写真を書こうと思う。 自然言語に学ぶ Perlのやったように、自然言語に学ぶことは多いと思うので、自然言語の持つ性質をいろいろ…

糖衣がけのMoonScriptはいかが?

MoonScriptが気に入ったので、構文について色々書き散らしたいと思う。解説記事とか入門記事じゃないよ。文法知りたい人はリファレンス読みましょう。 (MoonScript v0.2.2 - Language Guide) MoonScriptとは Luaにコンパイルするスクリプト言語。現時点での…

GObject Introspection

GObjectIntrospection - GNOME Live! GObject Introspectionはスゴイヤツである。こいつがあれば、GObjectを使っているC言語のライブラリへのバインディングを自動的に生成してくれる。今までだったら、言語ごとで個別にバインディングを作成しないとダメな…

Sui ― GUI Library for LÖVE (1) フォーカス

LÖVEでゲームを作ろう 3 簡単なUI - M59のブログ LÖVEでゲームを作ろう 4 クロージャー - M59のブログ 上の2つに次いで、3つ目のSuiの記事。今日はフォーカス機能を実装した。これがあれば、フォーカスのあるウィジェットだけ反応するようにもできる。前回書…

LÖVEでゲームを作ろう 3 簡単なUI

(簡単なUIとは使うのが簡単というより作りが簡単という意味) LÖVEで使えるGUIライブラリはCategory:Libraries - LOVEにいくつか載っているのだけれども、自分で簡単なGUIライブラリを作ってみることにした。 成果物: mandel59/lovesui · GitHub コードを抜…

LÖVEでゲームを作ろう 2 ゲームを実行したまま開発するには

Luaを使ったゲーム開発の利点は、コンパイルの必要がなく、コードを書き換えたらその場ですぐに試せることだ。 LÖVEでは、次のコードを使って、動的にLuaを読み込むことができる。 -- これはコードを読みこむだけで、まだ実行されない。 chunk = love.filesy…

LÖVEでゲームを作ろう 1 日本語でこんにちは

LÖVEはオープンソースの2Dゲームエンジンで、Lua言語でゲームを創ることができる。作ったゲームはWindowsとMac OS X、Linuxで遊ぶことができる。 MOONGIFTの記事: Luaで作る2Dゲーム「LÖVE」|オープンソース・ソフトウェア紹介を軸としたITエンジニア、Webデ…

作業ログだけ。 Flapjax – Functional Reactive Programming in Javascript | Continuous Learning Functional Reactive ProgrammingをJavaScriptでやる 円 ベジェ 近似 - Google 検索 円をベジエ曲線で近似する

Diagramsを使って円周率をモンテカルロ法で計算する

Using queries Diagramsのqueryを使うと、点が図形の内部にあるか外部にあるかが判別できる。 > {-# LANGUAGE NoMonomorphismRestriction #-} > > import System.Random > import Data.Monoid > import Control.Applicative > import Diagrams.Prelude > imp…

HaskellのDiagramsライブラリ

今日はDiagramsのことを知った。Diagrams - About diagrams DiagramsはHaskellで使えるベクターグラフィックス・ライブラリを生成するためのドメイン特化言語。ギャラリーを見ると、どんなことができるか少しだけ分かる。チュートリアルの最初の例。 {-# LAN…

Rust 0.4

以前もRustを取り上げた。(プログラミング言語 Rust - M59の記録) 先月(2012年10月15日)バージョン0.4がリリースされていたので、同じプログラムをもう一度書いてみる。 // for Rust 0.4 // Rust 0.1のuseはextern modに変更された // extern modはクレイト…