Idrisの話とIdris2のウワサ

2019-09-21

# Idrisの話とIdris2のウワサ 
----------------------
[Proof Summit 2019](https://proof-summit.connpass.com/event/141191/)

===
# About Me
---------
![κeenのアイコン](/images/kappa.png)

* κeen
 * [@blackenedgold](https://twitter.com/blackenedgold)
 * Github: [KeenS](https://github.com/KeenS)
 * GitLab: [blackenedgold](https://gitlab.com/blackenedgold)
 * [Idein Inc.](https://idein.jp/)のエンジニア
 * Lisp, ML, Rust, Shell Scriptあたりを書きます

===
# Idris
-------

* Edwin Brady 2013 〜
* 証明支援系ではなくてプログラミング言語
* 依存型のあるHaskell
* Eager Evaluation
* コンパイルするとバイナリが出る
  + C経由
  + JSバックエンドなども

===

# Hello, Idris
--------------

```idris
main : IO ()
main = putStrLn "Hello"
```

---

``` console
$ idris -o hello hello.idr
$ ./hello
"Hello"
```

===
# 依存型
---------------

* 値を型に書ける

```idris
data Vect :
  (len : Nat)
  -> (elem : Type)
  -> Type
where
  Nil  : Vect Z elem
  (::) : (x : elem)
         -> (xs : Vect len elem)
         -> Vect (S len) elem
```

---

```idris
v : Vect 3 Int
v = [1, 2, 3]
```

===
# 依存型
---------------

* 型で計算がでる

```console
append: Vect n a
        -> Vect m a
        -> Vect (n+m) a
append [] y = y
append (x :: xs) y = x :: append xs y
```

===
# 依存型
---------------

* 値として型を書ける

```idris
the : (a : Type) -> a -> a
```

---

``` idris
λΠ> 1
1 : Integer
```

---

``` idris
λΠ> the Double 1
1.0 : Double1
```

===
# 型と型の型
------------

* `(a : Type)` って何
* `a` : 名前
  + Idrisでは型シグネチャにも名前が書ける
* `Type` : `a` の型
* `Type` 型の値
  + `Int`
  + `Double`
  + `Vect 3 Int`
  + …

===
# 型と型の型
------------

* `Type` の型は？
  + → `Type 1`
* `Type 0` (=`Type`), `Type 1` , `Type 2` … と続く
  + Idrisの文法上は `Type n` とは書けない
* (Demo1.idr)

===
# 証明の話
----------

* もちろんカリー・ハワード対応で証明が書ける
  + プログラミング言語と論理学に対応関係がある
  + 型 ⇔ 命題
  + プログラム ⇔ 証明
  + …
* Idrisには依存型がある→述語論理の証明が書ける
* 多少証明専用の機能もある

===
# Modus Ponens
--------------

* $A \to (A \to B) \to B$
* 大文字は定数扱いなのでカインド宣言 `{A, B: Type}` を挟んでおく

```idris
total
modusPonens : {A, B: Type}
              -> A
              -> (A -> B)
              -> B
modusPonens a ab = ab a
```

===
# `partial` と `total`
----------------------

* 一般にプログラムが停止するかは判定できない
* Idrisは型にプログラムを書ける
* → コンパイル終わるの？
* → 証明として見たときに循環論法になったりしないの？
    ``` idris
    specialTheorem : {A, B: Type} -> A -> B
    specialTheorem x = specialTheorem x
    ```

===
# `partial` と `total`
----------------------

* 関数に `partial` や `total` の修飾子を付けられる
  + デフォルトで `partial`
* `total` を付けるとIdrisが停止すると確認できるものしかコンパイルが通らない

===
# `partial` と `total`
----------------------

``` idris
total
specialTheorem : {A, B: Type} -> A -> B
specialTheorem x = specialTheorem x
```

---

```console
   |
21 | specialTheorem x = specialTheorem x
   | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Main.specialTheorem is possibly not total due to recursive path Main.specialTheorem --> Main.specialTheorem
```

===
# `partial` と `total`
----------------------

* 再帰でもこっちは通る
  + 構造的に最初の引数が小さくなってるから

``` idris
total
append: Vect n a
        -> Vect m a
        -> Vect (n+m) a
append [] y = y
append (x :: xs) y = x :: append xs y
```

===
# 型環境とHole
--------------

* プログラムの一部を未完成のまま(=Hole)コンパイルできる
* `?ident` でHoleを作れる
    ```idr
    map : List a -> (a -> b) -> List b
    map xs f = ?hole
    ```
* IdrisがHoleの型を教えてくれる

===
# 型環境とHole
--------------

```idr
map : List a -> (a -> b) -> List b
map xs f = ?hole
```

---

```console
              b : Type
              a : Type
             xs : List a
              f : a -> b
     --------------------
           hole : List b
```