Idris面白機能:シンタックスシュガーとオーバーロード、あとユーザ定義構文

このエントリはIdris Advent Calendar 2020の17日目の記事です。

κeenです。今回は小ネタとしてシンタックスシュガー(糖衣構文)やオーバーロードについて紹介します。 あとIdrisにはユーザが構文を拡張できる機能もあるのでそれも紹介します。

if

Idrisでは if expr1 then expr2 else expr3 が糖衣構文として定義されています。 では展開すると何になるかというと、 ifThenElse 関数です。 「えっ?無理じゃない?」と思った方、正しいです。普通の言語では if は関数では書けません。 しかしIdrisでは関数で書けるのです。

昔紹介したようにIdrisではLazyという機能を使うと遅延評価ができます (IdrisはHaskellと違ってデフォルトではEager Evaluationをします)。 この Lazy を使って ifThenElse 関数はこう定義されています。

ifThenElse : Bool -> Lazy a -> Lazy a -> a
ifThenElse True  t e = t
ifThenElse False t e = e

ところで、Idrisでは関数をオーバーロードできるのでした。 ifThenElse をオーバーロードするとどうなると思いますか? そう、 if 式をオーバーロードできるのです。 少し試してみましょう。

以下の関数を定義します。

ifThenElse: Maybe a -> (a -> b) -> Lazy b -> b
ifThenElse (Just a) f _ = f a
ifThenElse Nothing _  b = b

これを読み込んだREPLでは Maybe 型の式に対して if が使えます。

Idris> if Just 1 then (+1) else -1
2 : Integer
Idris> if Nothing then (+1) else -1
-1 : Integer

面白いですね。

因みにLazyの記事で紹介しましたがショートサーキットする論理積の &&Lazy を使ったただの関数です。 Idrisでは演算子もユーザが定義できるのでこういった部分もユーザランドで定義できてしまうんですね。

do 記法

do 記法もシンタックシュガーです。 以下の do 式は

do
x <- hoge
y <- fuga x
z <- piyo y
pure $ chun z

以下のように展開されます。

hoge   >>= (\x =>
fuga x >>= (\y =>
piyo y >>= (\z =>
pure $ chun z
)))

ここで (>>=) もオーバーロード可能なので変テコな定義も可能なはずなんですが、パースエラーになってしまいました。

(>>=) : String -> a -> String
(>>=) s _ = s


hoge : String
hoge = do
  "This is string"
  "Others will be ignored"
  ["Nothing Happen"]
Type checking ./doNotation.idr
doNotation.idr:6:8-9:20:
  |
6 | hoge = do
  |        ~~ ...
Incomplete term do "This is string"
                   "Others will be ignored"
                   ["Nothing Happen"]

Holes: Main.hoge

謎です。

その他モナド関連記法

Idrisには何故か do 記法と役割の被る構文がいっぱいあります。

以下の関数を書き換えながら紹介します。

addDo : Maybe Int -> Maybe Int -> Maybe Int
addDo xs ys = do
  x <- xs
  y <- ys
  pure $ x + y

内包表記

以前リスト内包表記と紹介しましたが、より一般にはモナド内包表記です。 例えば Maybe に対しても使えます。

addComplehensions : Maybe Int -> Maybe Int -> Maybe Int
addComplehensions xs ys = [x + y | x <- xs, y <- ys]

ガード式も書けるんですが、Alternativeに触れないといけなくなるのでここでは流します。

! 記法

もうちょっと簡潔に書く方法として ! 記法もあります。

addBang : Maybe Int -> Maybe Int -> Maybe Int
addBang x y = pure $  !x + !y

熟語括弧(idiom brackets)

これはMonadではなくApplicativeの記法です。

addBracket : Maybe Int -> Maybe Int -> Maybe Int
addBracket xs ys = [| xs + ys |]

これは以下に同じです。

addBracket : Maybe Int -> Maybe Int -> Maybe Int
addBracket xs ys = (+) <$> xs <*> ys

これはまあ、分かる。

ユーザ定義構文

Idrisには中置演算子をユーザが定義できる機能があるというのはAdvent Calendarで紹介した通りですが、もうちょっと一般にn項演算子を定義する機能があります。syntax 構文.... = 内容 の構文です。構文のところにはダブルクォートで囲ったキーワード ("キーワード")か、式を表わす [仮引数] 、 変数を表わす {仮変数} が書けます 1

内容のところにはIdrisの式を書きます。

if then else は既にあるので unless then else を定義してみましょう。

syntax "unless" [test] "then" [t] "else" [e] = ifThenElse test e t
Idris> unless True then 1 else 2
2 : Integer
Idris> unless False then 1 else 2
1 : Integer

次に変数を使うユーザ定義構文も定義してみましょう。 for 式です。

syntax for {x} "in" [xs] ":" [body] = forLoop xs (\x => body)

forLoop : List a -> (a -> b) -> List b
forLoop l f = map f l

{x} と仮変数を使っていますね。

REPLで試すと動いているのが分かります。

Idris> for x in [1, 2, 3]: x + 1
[2, 3, 4] : List Integer

因みに syntax で定義した構文はパターンとしても使えます。 例えば以下のように定義すると、 SomeJust の代わりに使えます。

syntax "Some" [x] = Just x
syntax "None" = Nothing

パターンとして使うときはこうですね。

hoge : Maybe Int -> Int
hoge x =
  case x of
    Some x => x
    None => -1

値として使うときはこうです。

Idris> hoge (Some 1)
1 : Int
Idris> hoge None
-1 : Int

パターンでだけ、値でだけ定義したいときは pattern syntaxterm syntax という構文もあります。

詳しくは syntax rulesのドキュメントを参照して下さい。文法にあいまい性が生じそうなケースはエラーになるようです。

リテラルのオーバーロード

\x => body と書いたらユーザ定義データの Lambda x body になったり f x と書いたら App f x になったりのヤバそうな機能もあるようです。詳細は論文読んでねスタイルなのでここではスルーします。

興味のある方は dsl notationのドキュメント を読んでみて下さい。

まとめ

Idrisのシンタックスシュガーとそれをオーバーロードする方法を紹介しました。 また、 syntax rulesというn項演算子を作れる機能も紹介しました。


  1. ドキュメントには言語のキーワードならダブルクォートなしで書けるとあるのですが、実際に試したらエラーになりました。 [return]
Written by κeen
Older article
SMLのDerived Forms