ElixirはErlang VM (BEAM) の上で動作するRubyライクな文法をもつ関数型言語として知られています。
Erlangと同様に値は全てイミュータブルですが、Erlangが再束縛(再代入)不可である一方、Elixirは再束縛(再代入)可という異なるアプローチを採用しています。
再束縛(再代入)の可否を選択できる言語においては、正当な理由がない限り再束縛(再代入)不可の利用が推奨されており、Elixirのアプローチは一見悪手のように見えるかもしれません。
なぜElixirの再束縛(再代入)可という選択が悪くない戦略なのかについて、関数型言語の特性や、束縛、代入、ミュータブル、イミュータブル等の整理を通じて紐解いてみたいと思います。
Excel 2021でLAMBDA関数が実装されてExcelの数式はチューリング完全になるとともに、MAP、REDUCE関数などの関数型プログラミングでよく使われる関数も実装されました。
また、Excelは、数式は常に返り値を持つことに加え、データは完全にイミュータブルで、ほとんどの場合に参照等価性を持っているなど、関数型言語としての特徴も有しています。
そこで、今回のセッションでは、Excelを使って関数型プログラミングの初歩的な処理をする方法を紹介しようと思います。
定理証明支援系であり純粋関数型プログラミング言語でもある、Lean について紹介します。
Lean はまだ新しい言語であり知名度も低いので、このトークではLean言語の名前と特徴を憶えてもらうことを目標とします。
XSLTはXMLを変換するためのテンプレート言語ですが、関数型プログラミング言語とよく似た特徴を持っています。
本発表では、XSLTを関数型言語として捉え、実際にBrainfuck処理系を実装した事例を紹介します。
テンプレート適用によるパターンマッチ、変数の不変性、再帰的な処理といった関数型的な特徴を活用し、
ループや状態管理をXSLTでどのように記述できるかを具体的なコードとともに解説します。
Brainfuckのようなチューリング完全な処理系を実装できることから、XSLTもチューリング完全なプログラミング言語であることを示します。
この実装を通じて、関数型プログラミングの視点を広げるきっかけになれば幸いです。
型システムはある種のバグを静的に検査可能な手法で、多くの型システムは健全性を満たします。つまり、型システムが言うことは全て正しいです。
一方で、実世界の型システムは、ひょんなことから健全性を破壊する「穴」が存在していたりします。怖いですね。
本トークでは、Java や Rust、OCaml など、実世界のプログラミング言語における型システムの「穴」を概観します。罠を事前に知ることで、実際にハマったときの素早い対処や、プログラミング言語への深い理解が期待されます。
LISPは記号処理に特化して初期の人工知能研究を牽引した言語であり、実用的な関数プログラミングを提供した最初の言語といえるでしょう。
現在のLisp族の末裔たちも関数プログラミングのための機能を備えている一方、後続の関数型言語(ML族)が持つ静的型や参照透過性、モナドなどの機能は持っていません。
このトークでは日常的にEmacsとEmacs Lispを利用しているユーザーが、Lispのどのような側面が「関数型」的で、なぜ関数型言語ではないと考えているのか、Emacsを用いたプログラミングの実践とEmacs Lispの「正体」までお話しします。
医療業界向けに複数のSaaSプロダクトを提供するコンパウンドスタートアップ「カケハシ」では、OIDC (OpenID Connect) 対応の共通認証基盤を開発・運用中です。OIDC対応の認証基盤の開発では、画面をまたぎながら多様なパラメータを取り扱うため、不正な状態遷移やバリデーション漏れが大きなセキュリティリスクとなります。本セッションでは、TypeScriptで代数的データ型 (Algebraic Data Types; ADT) を活用し、以下のような特徴的なポイントを押さえて実装した事例を紹介します。
OIDCを利用した認証フローでは、多数のパラメータを扱う複雑なバリデーションが要求されるうえ、アカウント選択→認証→同意といったステップを画面遷移を伴いながら進める必要があるため、状態管理も非常に煩雑になります。
そこで、 「アカウント選択済み」「認証中」「同意完了」など、認証フローの状態と振る舞いを代数的データ型で表現します。これにより、型システムを活用して不正な状態遷移(例: 同意せずに認証を終了、画面Aをスキップして画面Bに直行してしまう)を排除できます。
代数的データ型は、バリデーション漏れの防止にも有効です。様々なユースケースで利用できるように設計されたOIDCでは、数多くのパラメータをバリデーションする必要があります。
そこで、バリデーションの状態を代数的データ型で表現することで、不正なパラメータが渡されることを防止します。
Coqには、証明付きプログラミングを容易にする Program 機構があります。本LTでは、この Program 機構の概要とその利用例を紹介します。
この機能を紹介する題材として、インデックスを用いたリストの要素取得を取り上げます。Coq において、指定したインデックスにあるリストの要素を取得する場合、通常は option
型を返すか、指定したインデックスに要素がない場合に備えて、あらかじめデフォルト値を渡す必要があります。しかし、指定したインデックスがリストの長さ未満ならば、毎回 Some
が返ってくることは明らかです。
本LTでは、Program 機構を活用し、インデックスがリストの長さ未満であることが前提の場合に、option
型を用いず、またデフォルト値を与えることなくリストの要素を取得できることを紹介します。「Coqにこんな機能があるのか!」と興味を持ってもらえたら幸いです。
関数型プログラミングと聞いて、初心者の方が一番に連想するキーワードは"純粋関数"ではないでしょうか。
一方で、純粋関数を作るうえで"副作用を受けない・スコープが決まっている値"というのは非常に重要ですが、この概念=代数的データ型についてはまだそれほど広まっていないように思います(主観)
そこで、このセッションではKotlinを用いて直積型と直和型から始まり、enumとSealed classとの違いについてまでお話しします。
私のブログサイト https://blog.pizzacat83.com を作るために F# でジェネレータを実装した話です。このブログサイトはFornaxという静的サイトジェネレータをforkしたジェネレータで生成しています。
Fornaxは、データの読み込みやサイトの生成処理を F#スクリプトで書くと、それを実行してサイトを生成してくれる、というものです。これにより、以下のメリットがもたらされます。
データ読み込みやサイト生成をF#スクリプトで表現するからこそ、データソースとしてファイルから読み込むことも、headless CMSのAPIを叩くこともできます。サイト生成処理の中ではMarkdownをHTMLに変換することも、Markdown一式からRSSを生成することも、自在に実装できます。そしてこれらの処理をすべて F#で実装するので、F#の型システムの恩恵を存分に享受できます。補完のないままテンプレート言語を書いて実行時エラーに悩まされる必要はないのです。
セッションでは以下について話す予定です。
なお、Fornaxの使い方や私がFornaxを選定した背景などは、ブログ記事「F#でこのブログを構築した」に綴っています。セッション内で語りきれなかったテーマについても、懇親会などでぜひお話ししましょう!