タグ

ブックマーク / blog.miz-ar.info (19)

  • 子供が生まれた/後進を育成すること | 雑記帳

    9月に子供が生まれました。出産に立ち会いましたが、にとっては文字通り命懸けで、感謝してもしきれません。父親として、と共に子育てを頑張っていきます。 今は育休をとって二人で世話をしています。職場では私はそれなりに重要なポジションなので、休むと他の人が頑張らないといけません。復帰した後は、迷惑をかけた分を挽回できるように頑張りたいところです。 それにしても、自分の子供というものは思った以上に可愛いものです。見ていて飽きません。穏やかに寝ていたら「寝る子は育つ!えらい!」、泣いていたら「赤ちゃんは泣くのが仕事!えらい!」、手足をバタバタ動かしていたら「筋トレだ!えらい!」、排泄をしたら「生命活動の証!えらい!」という具合です。親バカでしょうか。 この子がどんな大人に育つのか、その時の社会はどうなっているのか、わからないことだらけですが、少しでも良い未来になるようにできることをしたいです。 子

    igrep
    igrep 2025/10/28
    めでたい!そして偉い!
  • 定理証明支援系についての問題意識 | 雑記帳

    定理証明支援系 (proof assistant / interactive theorem prover) というのは、専用の言語で書いた証明を機械にチェックさせるツール、およびその証明の記述を支援するツールです。Rocq(旧名Coq)、Agda、Lean、Isabelleなどが有名です。 この記事では、定理証明支援系について私が感じている問題意識を説明します。私自身は定理証明支援系のヘビーユーザーではないので、もっと勉強したり、定理証明支援系を使い込んだりすれば答えが見つかるのかもしれません。詳しい方からのフィードバックを頂けると嬉しいです。 このブログでは、過去に定理証明のできる依存型プログラミング言語Idrisを使った定理証明を扱いました。10年以上前ですが……。 Idrisで遊んでみた (0) (2014-02-27) Idrisで遊んでみた (1) (2014-02-27) I

  • 「関数の副作用の有無」よりも大事なもの | 雑記帳

    プログラミングをやっていると、「関数に副作用がある」とか「副作用がない」あるいは「純粋である」という話をちょいちょい耳にする。そして、「外界の状態を読み取るけど変更はしない関数」、例えば function getTime() { return Date.now(); } のような関数に副作用があるか?みたいな議論が始まったりする。 くだらない議論だ。 何か概念を定義するときは、それが「役に立つ」場面を提示できる必要がある。「関数の副作用」を定義するときは、「関数の副作用」がわかったときに何をしたいのかをはっきりさせる必要がある。「関数のどういう側面に注目したいか」を決めずに「副作用の有無」を論じるのはナンセンスだ。 ここでは、言語処理系(コンパイラー)を実装する者の立場で、関数の副作用について論じてみたい。 一般に、「副作用がない」関数の呼び出しは、「副作用がある」関数の呼び出しに対するも

  • GHCへの私の貢献2023 | 雑記帳

    この記事は Haskell Advent Calendar 2023 の6日目の記事です。 私はここ数年、HaskellコンパイラーであるGHCに貢献しています。この記事では、今年(2023年)に私が行った貢献を紹介します。 GHCの開発は独自ホストされたGitLab上で行われています。 Glasgow Haskell Compiler / GHC · GitLab 私の貢献 今年は貢献と言っても、バグ報告のみ(修正パッチは含まない)のケースが多いです。私はLunarMLが忙しいので……。 FMAについてコメント(2月ごろ) 2〜3月ごろに、FMA (fused multiply add) を計算するプリミティブをGHCに実装するマージリクエストが出ていました。 !9996: Add fused multiply-add operations · Merge requests · Glas

    igrep
    igrep 2023/12/06
    素晴らしい
  • Haskell/GHCのSIMDについて考える | 雑記帳

    最近のコンピューターの性能を活用するには、何らかの並列化が必須です。具体的にはSIMDの活用やマルチコア(それとGPU)です。プログラミング言語でこれらを利用できれば「C言語よりも速い」を名乗れます。この記事では並列化技術のうち、SIMDを考えます。 HaskellコンパイラーであるGHCにはSIMDのプリミティブ(データ型と関数)が実装されています。しかし、広く使われているとは言い難いです。 使いづらい要因はいくつか考えられます。使えるバックエンドの少なさが一つで、現状(GHC 9.8時点)では、x86(_64)向けのLLVMバックエンドでしか使えません。AArch64など他のアーキテクチャーや、NCGバックエンドでは使えません。 別の要因として、用意されたプリミティブが少ないというものがあります。例えば、整数のビット演算はできません。 現状 論文 GHCにSIMDプリミティブを実装した

    igrep
    igrep 2023/08/18
  • LunarML進捗:signatureの実装に向けて | 雑記帳

    自作SML処理系進捗:Hello Lua! の続き。 自作SML処理系「LunarML」の言語機能の実装も佳境に入ってきて(equalityやexception等の厄介な奴らはだいたい片付けた)、残すところは withtype (derived form)abstype(Successor MLに従いderived formとして実装する予定)signaturefunctor くらいとなってきている。 derived formはいつでもできるとして、未実装の機能のうち大きなものがsignatureとfunctorだ。このうちfunctorはsignatureに依存するので、signatureを先に実装することになる。 第一級モジュールの動機 それとは別に、モジュール関連の実装したい機能として、第一級モジュールに相当する機能を入れたい。これのモチベーションは標準ライブラリーを実装するための実

  • 限定継続いろいろ | 雑記帳

    このブログでは限定継続について過去に何回か記事を書きました: LunarMLと継続限定継続と例外とモナド 今回、LunarML向けのVMに限定継続を実装してみて理解が深まったので、改めて記事にします。 限定継続:スタックを使ったざっくりとした説明 今回はスタックを使って限定継続をざっくりと説明してみます。 関数という概念を持つプログラミング言語では、スタックを使って関数の呼び出しを管理することが多いです。コールスタックとか、スタックのバックトレースとか言いますよね。ここではネイティブのスタックか仮想マシンのスタックかというのは問いません。 関数を呼び出すと、フレームと呼ばれる領域がスタックに確保されて、関数への引数やローカル変数はそこに確保されたりします。 例えば、以下のプログラムを考えます: void g() { // すごい計算 } void f() { double j; g();

    igrep
    igrep 2022/10/30
    LunarML, Wasm stack-switching proposalを試しに実装するのに良さそう(どっちも詳細詳しくないので知らんけど)
  • 執筆中:「Haskellでの型レベルプログラミング」 | 雑記帳

    最近、「Haskellでの型レベルプログラミング」という「」を執筆している。まだ完成ではないが、以下のリンクから読める: Haskellでの型レベルプログラミング なぜHaskellか 最近いろんな言語が出てきている中で、Haskellの強みとは何だろうか。人によって答えは色々あるだろうが、筆者にとってHaskellの魅力的な側面は強力な型システムである。どのくらい強力かというと、型レベルでプログラミングができ、依存型の模倣さえもできてしまう。 (依存型をやりたいなら最初から依存型のある言語を使えという意見は尤もだが、それはそれとして。) Haskellでの型レベルプログラミングの解説記事というのは、英語圏ではちらほら見かけるが、日語圏ではあまり見ない。2018年(原文は2017年)に公開された Haskellにおける型レベルプログラミングの基(翻訳) – Qiita が数少ない例で

  • GHCのバックエンドについて | 雑記帳

    先日リリースされたGHC 9.2.1で、64ビットArm(AArch64)向けのネイティブコード生成器(Native Code Generator; NCG)が実装された。これを機会にGHCのバックエンドについて簡単にまとめてみる。 概略 GHCでHaskellプログラムをコンパイルすると、いくつかの中間言語を経て最終的には機械語が出力される。 この工程の最後の部分を「バックエンド」と呼ぶ。 GHCには Native Code Generator (-fasm)LLVM backend (-fllvm)unregisterised via-C backend の3種類のバックエンドが存在する。このほか、バイトコードインタープリターと-fno-codeもデータ型的にはバックエンドの一種として扱われている。(参照:compiler/GHC/Driver/Backend.hs) Native C

    igrep
    igrep 2021/11/01
  • GHCいじくり日誌・AArch64編 | 雑記帳

    ここ数日またGHCをいじっている。少し前にAArch64 NCGがマージされたのでその確認という意味が大きい。 前回の記事(3月):GHCに初めてコントリビュートした/最近のGHC動向 同ジャンルの記事(2020年10月):GHCデバッグ日誌 abs関数とNaNの符号ビット 自作ライブラリーfp-ieeeのテストを(Gitから取ってきた)最新のGHCで動かしてみたら引っかかるものがあった。 fp-ieee: IEEE 754-2019 compliant operations どうやら、筆者のコードが「Float/Doubleに関するabs関数が符号ビットを常にクリアする」ことを期待しているのに対し、AArch64 NCGを使った場合はNaNの符号ビットがクリアされないようだ。 数日前に、絶対値関数の実装についての話がツイッターに流れてきた: 話題になった記事では「ゼロの符号を考慮しろ」と

    igrep
    igrep 2021/08/29
    “11月7日にHaskell Day" "筆者はそこで「GHCの動向2021」と題して話すことになりました。動画の提出締め切りが9月後半なので最新情報をどこまで盛り込めるか不確定なのですが、なんとかがんばります” 🙏
  • GHCに初めてコントリビュートした/最近のGHC動向 | 雑記帳

    事実上の標準デファクトスタンダードなHaskell処理系であるGHCに貢献するというのが去年掲げた目標だったが、それがようやく実現したので報告する。ついでに、最近のGHC開発状況についても簡単にまとめてみる。 「貢献」と言っても色々あって、バグ報告とかも立派な貢献なのだが、ここで目標としていたのは「書いたコードをGHC体に取り込んでもらう」ことである。 一つ目:fromInteger :: Integer -> {Float,Double} 年末に書いた記事 Haskell/GHCでの浮動小数点数の扱い – Qiita にあるように、現行のGHCのfromIntegerは値の大きさによって丸め方法が違っている。それによってどういう問題が引き起こされるかというと、 import Numeric import Data.Word main = do putStrLn $ "literal :

  • PureScript 雑感 | 雑記帳

    PureScript は、 Haskell ライクな altJS である。「Haskell ライク」という評判に劣らず、 Haskell の最も重要な特徴である型クラスをきちんと受け継いでいる。 現在のバージョンは 0.11.7 である。したがってまだ安定しているとは言えない。バージョン 1.0 まで解決されるべき Issues はこれだけある。 特徴 Haskell との設計上の違いは、以下のページにまとまっている: documentation/Differences-from-Haskell.md at master · purescript/documentation その中でも大きなものを、筆者の独断と偏見で2つ挙げる: 正格評価 レコード型と row polymorphism その他の特徴: Rank N polymorphism (RankNTypes) がある MultiPa

  • QuickCheckで競プロ用Haskellコードをデバッグする | 雑記帳

    競技プログラミングでは、提出したプログラムが誤答(WA)だった場合に「どのような入力について」答えを間違えたのか(参加者には)分からないことが多いです。 こういう場合はエスパーするなり眼力でソースコードをぐっと睨んだりするとバグが発見できる場合もありますが、初心者にはそういうのは難しいでしょう。 この記事では、HaskellのQuickCheckというライブラリーを使って、「ランダムにテストケースを生成して素朴な解と一致するか」を自動で検証させます。QuickCheckはテストに失敗した場合に「どういう入力例に対して失敗したか」も教えてくれるので、デバッグにも役立ちます。 この記事は筆者が先日YouTubeに上げた動画を文章で書き直したものです。動画で触れられなかった・触れるのを忘れていた補足説明みたいなものも若干含んでいます。この記事と動画、両方見ていただけると嬉しいです。 今回取り上げ

    igrep
    igrep 2020/08/27
    それでなくても==>を使うとテストが遅くなりがちなんで全く使ってないなぁ
  • 最速のフィボナッチ数計算を考える | 雑記帳

    Qiitaにこういう記事を書いた: Haskellでフィボナッチ数列 〜Haskellで非実用的なコードを書いて悦に入るのはやめろ〜 ↑の記事ではメモ化しない計算法が遅いこと、Haskellには遅延評価の罠があって正格にすると早くなること、「n番目のフィボナッチ数」をピンポイントで計算する場合は(行列またはQ(√5)の)冪乗を使う方法が早いこと、一般項(ビネの公式)をその辺の浮動小数点数で計算するのは使い物にならないこと、などを述べた。 まあ、「Haskellでは fib 0 = 0; fib 1 = 1; fib n = fib (n-1) + fib (n-2) でフィボナッチ数が計算できます!」に対する注意喚起としてはこれで十分すぎる内容なのだが、「n番目のフィボナッチ数をピンポイントで計算する方法」についてはもっと深掘りできる。 この記事では、数学的な考察も交えて、「n番目のフィボ

    igrep
    igrep 2020/04/22
  • Haskellのscan系関数を使いこなす | 雑記帳

    Haskellはリストを操作する関数を多数提供しています。map, filter, foldあたりが代表的で、これらは他の言語でもおなじみかと思います。 一方で、scan系関数(scanl, scanr)は他の言語ではあまり見かけない気がします。同じ関数型言語のSMLやOCamlにも標準では入っていないようです。 この記事では、scan系関数がどういう場合に利用できるかを紹介します。 scan系関数とは 定義と図解 scan系関数は、リストを元にして新しいリストを構築する関数です。新しいリストの要素は、与えられた初期値と関数を使って元のリストを途中まで畳み込んだものになります。「foldの途中経過を残す版」とでも言えば良いでしょうか。 型はそれぞれ次のようになります: scanl :: (b -> a -> b) -> b -> [a] -> [b] scanr :: (a -> b ->

    igrep
    igrep 2019/10/17
    具体的なAtCoderの問題例に加えて自著の宣伝まで巧みに挟まれててすごい。
  • Haskellerのためのモノイド完全ガイド | 雑記帳

    Haskellにおけるモノイドについて解説記事を書いてみた。他の言語でも通用する話があるかもしれないし、ないかもしれない。 モノイドとは モノイドとは、ざっくり言うと「くっつける」演算ができる対象のことである。例えば、文字列やリストの連結、数の足し算や掛け算は「くっつける」演算の一種である。 モノイドには「くっつける」演算の他にもう一つ条件があって、モノイドは「くっつけても何も起こらない値」を持っていなければならない。例えば、文字列の場合は空文字列、リストの場合は空リスト、数の足し算の場合は0、掛け算の場合は1、という具合である。 というわけで、文字列、リスト、数の足し算、数の掛け算はいずれもモノイドの具体例である。ただし、同じ数の集合(整数、など)を考えていても、演算が異なる(足し算 vs 掛け算)場合は、異なるモノイドとみなす。 モノイドの定義をちゃんと書くと、モノイドとは集合 \(M

    igrep
    igrep 2019/02/12
    Ap Monoid知らなかった。
  • Haskell で高速なプログラムを書くときに注意すること | 雑記帳

    Haskell は表現力が高いプログラミング言語だが、気をつけないと非効率的なコードが生成されてしまうことがある。では、どういうところに気をつければ高速なコードになるのか。少し調べてみた。 この記事に書くのは、あくまで原則とかそういうやつなので、コンパイラーの最適化(正格性解析、インライン化、自動ボックス化解除)によっては、自前で工夫しても意味がない、つまり、コンパイラーに任せた場合と同じ結果になるかもしれない。どういう場合に早くなるかはケースバイケースなのだ。 ここで扱うトピックは大きく分けると、 正格評価 型クラスの特殊化 Unboxed 値 その他 となる。あくまで自分用の備忘録であり、特に突飛なことを書いているつもりはないので、知ってる人はアーハイハイという感じで読み飛ばしてしまえるだろう。また、筆者の理解が浅く、誤解に基づいたことを書いているかもしれないので、あまり信じすぎないよ

    igrep
    igrep 2019/02/07
    "型クラスは便利だが、型クラスを使うと関数呼び出しの際にコストが発生する。実態としては C++ の仮想関数的な感じのはず" マジか。型で解決できるからコンパイル時に特殊化できそうなものなのに。
  • Haskell でのデバッグ手法あれこれ | 雑記帳

    プログラムにバグはつきものです。強力な型システムを備えている Haskell でもそれは同じです。この記事では、 Haskell プログラムのデバッグ手法をいくつか挙げてみます。 なお、使用している GHC は 8.2.2 です。より新しいバージョンで追加されるであろうより便利な機能は、この記事の対象外です。 【2018年2月8日 更新:-fexternal-interpreter, Control.Exception.assert, debug パッケージについて追記】 【2018年5月25日 更新:プロジェクトごとにPreludeを持っていると便利という話を追加】 心構え:処理を分割せよ Haskell は純粋な言語です。IOが絡まない関数であれば、同じ引数に対しては同じ結果が返ってくることが期待されます。 よって、処理を細かく(純粋な)関数に分割し、それぞれ GHCi で動作を確かめ

    igrep
    igrep 2018/01/25
    記事のコメントにも書きましたが、最近作られた https://hackage.haskell.org/package/debug も試してみてください!
  • 複素関数記述DSLについて | 雑記帳

    この記事は 言語実装 Advent Calendar 2017 7日目の記事です。 この記事では、私が作っているDSLの設計思想を主に書きます(実装が未完なので)。 以前、 複素関数で遊ぼう というWebアプリ(と言ってもサーバー側で状態を持たないのでほぼブラウザーアプリ)を作りました。このアプリでは、複素関数を表す数式をユーザーが任意に入力できます。 例:exp(z) 例:\sum_{n=1}^{10} z^n/n! 数式はHaskellで書いたパーサーで解釈し、JavaScriptへコンパイルしています。コンパイルしたJavaScriptはブラウザー側で実行させます。 関数のグラフを描くためには値を大量に計算する必要があるため、与えられた関数に対してなるべく効率の良いコードを生成することが一つの目標になります。 課題1:静的型をつけたい 対象が複素関数なので、扱う値というのは基的には

    igrep
    igrep 2017/12/08
  • 1