haskell-jp / beginners #18 at 2021-10-17 15:37:04 +0900

こんにちは、一つ質問をさせてください！
現在型安全に状態遷移を表現する方法について悩んでいます。

data State
  = Ready 'StateA -- 型の上で次の状態を指定すれば、型安全な状態遷移を実現できるのではないか
  | StateA [Text] 'StateB
  | StateB [Text] 'Finished
  | Finished [Text] '()

toStateA :: State -> Text -> State -- この型上で何かしらパターンマッチングをしないといけない？
toStateA (Ready 'StateA) text = -- 値でパターンマッチングをすることはできない
  StateA [text]

理解が足りず、実現する手がかりがありません……

型安全な状態遷移をするのに必要なことは
• 型に次の状態を入れ込む
• 関数のシグネチャで、特定の遷移先の情報を持っている型のみ引数に取るようにする
だと考えているのですが、どのように状態の型を定義すればいいか少々混乱しています。なにかお力添えいただけないでしょうか？

愚直にやるなら、単純に State 型の各コンストラクターをそれぞれ別の型にすれば良いかと思うのですが、それでは間に合わない事情があるのでしょうか。

@igrep さん
いつもご返信ありがとうございます。
現在を利用してTUIを作成しているのですが(前回回答いただいたプロジェクトです)、
すべてのstateを一つの型として定義する必要があり、

• data/newtypeで定義すると名前の重複
• typeで定義する際はunion typeが使えず
と言った具合で、どうにも実現できなかった次第です。
確実に私の理解・知識不足だと思うのですが、一寸先は闇状態で…
なにか常識的な解法がありそうだと踏んで質問させていただきました。

いやー、そんなに謙遜する必要もないです。
依存型などの仕組みが必要な問題なのでかなり面倒な問題です。常識的な解法は「ある意味でない」と私は思います。個人的には、そこで依存型を真剣に勉強して詰まるよりは、普通にランタイムエラーが起こるのを覚悟で作って試行錯誤した方がいいんじゃないかなぁと思います。Haskellの依存型はまだ完全なものではなく使いづらいですし...。もちろん、何をultimate goalとしてやっているのか次第で、依存型などのそうした技術を本当に勉強したいのであれば調べればいいと思います。そうでないなら、アプリができるよう手を動かしましょう。

なるほど…。そこまで高難易度な問題だったのですね。
確かに以前idrisや依存型等調べていたときに、プログラムの証明等沼に入り込むことになるからやめたほうがいい…
のような趣旨の文言を目にしました。

この問題は腰を据えて勉強するべきものなんですね。それがわかってよかったです！
現状最優先事項は型レベルプログラミングの勉強をすることではなく、完成させることなので続けて実装します！ありがとうございます！

私も似たようなことが必要になったので、
その時は、
data State hasA hasB みたいに型引数突っ込んで、
type ReadyA = State Identity Maybe みたいに具象化してました。

ありがとうございます！
今の私にはまだ何がわからないのかもわからないぐらいです。

なぜ型引数にmonadを突っ込んでいるのでしょうか？
kindも合わないような気がしてます。
なにか特別なやり方が隠されているんでしょうか……!

今回の件とは似てるけどちょっと違うので混乱を招いたかもしれません、それにかなり説明不足でしたね…申し訳ない。
前提条件としてデータAからデータBを導く関数fがあって、fはデータAを要求するため、関数の型定義として状態StateはフィールドとしてデータAは必ず持っているとしたいわけです。
そこでStateのフィールドは a :: hasA A としておいて、型引数hasAをIdentityとMaybeで切り替えれば、hasAがIdentityの場合は必ずフィールドaは持っていることが分かる、と言ったことを行っていました。

※すみません、途中まで書いて送信しちゃいましたが、やっぱり考えがまとまらなかったので消しました。

なるほど、ありがとうございます。ものすごい浅瀬からの意見ですが、これはHKDですか？
今朝たまたまhaskell荘園を見学していたら出てきました。

data State hasA hasB = State (hasA A) (hasB B)

data A = A Int String
newtype B = B Bool

type HasA = State Identity Maybe
type HasB = State Maybe Identity

d :: HasB
d = State Nothing (Identity (B True))

こんな感じで、外側から一定の性質を入れ込む方法なんですね。
私はまだ経験も知見も足りないので、こういう高度な事は過剰に使って複雑性を高めてしまいそうです笑
でも使ってみないことには適切な使用方法もわからないでしょうし、少し試してみようと思います！ありがとうございます！

↑ちょうどrandomにも上がっていますね！笑

HKDですねえ、ただ既存のライブラリが対応してるHKDは1,2引数で全てMaybeとか全てIdentityとかなのであんまり既存のライブラリを使えませんでしたね…

なるほど、ありがとうございます。
HKDというのは比較的新しいパターンということなんでしょうか？歴史的な経緯等は存じ上げないので見当違いかもしれませんが。

それはよく分かりません

失礼しました、ありがとうございます。