(wat-aro)

無職から有職者にランクアップしました

ActiveModel::Attributesでカスタムタイプを使う

Rails 5.2.0 で入ったActiveModel::Attributes API 最高ですよね。

でもカスタムタイプのドキュメントが見つからないんですよね。 ActiveRecord::Attributes API のカスタムタイプ ならあるのですが。

ソースコード見たところ簡単に作れるのがわかったので紹介します。

まず型の登録部分ですが、lib/active_model/type.rb で定義されています。

また、ActiveModelで使われているデフォルトタイプの実装を見ると cast_value メソッドがあればよさそうです。

ActiveRecord::Attributes API と同様に実装します。

class MoneyType < ActiveModel::Type::Integer
  def cast_value(value)
    if !value.kind_of?(Numeric) && value.include?('$')
      price_in_dollars = value.gsub(/\$/, '').to_f
      super(price_in_dollars * 100)
    else
      super
    end
  end
end

# config/initializers/types.rb
ActiveModel::Type.register(:money, MoneyType)

# app/models/store_listing.rb
class StoreListing
  include ActiveModel::Model
  include ActiveModel::Attributes

  attribute :price_in_cents, :money
end

store_listing = StoreListing.new(price_in_cents: '$10.00')
store_listing.price_in_cents # => 1000

このように ActiveModel::Attributes でカスタムタイプを使うことができます。

http-conduit で取得したデータを日本語表示する

簡単なcliツールを書こうとしたら http-conduit で取得したデータの日本語表示でハマってしまいました。

http-conduithttpLbs で取得したデータをそのままターミナルに出力します。
必要なパッケージは http-conduit bytestring utf8-string の3つ。

{-# LANGUAGE OverloadedStrings #-}

import qualified Codec.Binary.UTF8.String as Codec
import           Data.ByteString.Char8    (unpack)
import           Data.ByteString.Lazy     (toStrict)
import qualified Network.HTTP.Simple      as Simple

main :: IO ()
main = do
    res <- Simple.httpLbs "https://twitter.com/"

    putStrLn $ Codec.decodeString $ unpack $ toStrict $ Simple.getResponseBody res

httpLbs を使い取得したデータは Reponse 型で包まれているので getResponseBodyByteString を取得し、 String に変換して出力します。
なぜか ByteString でなく ByteString.Lazy になっていたので toStrict で変換。
そして unpack しても日本語が表示されないため、 Codec.Binary.UTF8.StringdecodeString で変換してから表示。

文字列難しい

[参考]

Haskellから簡単にWeb APIを叩く方法 - Qiita

Haskell 文字列変換入門 - Qiita

プログラミング Coq (証明駆動開発 2)

証明駆動開発入門(2)

上記ページの勉強メモです。

Extraction

coq から OCaml, Haskell, Scheme のコードを出力する。

OCaml にコードを出力するにはそのまま

Extraction map.

とすればいい。
これで

(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)

let rec map f = function
| Nil -> Nil
| Cons (a, t) -> Cons ((f a), (map f t))

と出力される。(proof-general を使っています。coq-ideの場合はcommand pane で実行)

この時、list が OCaml 組み込みのリストでなく coq で定義された list になっている。
OCaml 組み込みのリストを使うには

Extract Inductive list => "list" ["[]" "(::)"].

を実行する。こうすると

(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)

let rec map f = function
| [] -> []
| a::t -> (f a)::(map f t)

OCaml 組み込みのリストを使ったmap関数が生成される。

HaskellScheme に出力するにはそれぞれ
Extraction Language Haskell. Extraction Language Scheme. としてからOCamlの場合と同じように出力する。

Extraction Language Haskell.
Extract Inductive list => "list" ["[]" "(::)"].
Extraction map.
map :: (a1 -> a2) -> (list a1) -> list a2
map f l =
  case l of {
   [] -> [];
   (::) a t -> (::) (f a) (map f t)}

正しいけど、あまり綺麗なコードじゃない。

map :: (a -> b) -> (list a) -> list b
map f [] = []
map f x::xs = (f x) :: (map f xs)

くらいには変換してほしいけど、元の形からすると厳しいのかな。

次は scheme.

Extraction Language Scheme.
Extraction map.
(define map (lambdas (f l)
  (match l
     ((Nil) `(Nil))
     ((Cons a t) `(Cons ,(f a) ,(@ map f t))))))

おお。lambdas ってなんだ。match なんて RnRSにないぞ。というか、準クオート使ってるし、,使った式展開も入ってる。
Coq Extension Scheme っていうのがあって、lambdas マクロやmatch マクロ、@マクロが定義されているわけか。
lambdas マクロと @マクロはなかなかよい。
OCamlHaskell っぽく書きたい時は便利そう。
match マクロは define-syntax みたいな感じかな?
直接変換するならたしかにこういうマクロ欲しくなるな。

insertion_sort の変換

OCamlの場合

Extraction Language Ocaml.

Extract Inductive list => "list" ["[]" "(::)"].
Extract Inductive bool => "bool" ["true" "false"].
Extract Inductive nat => int ["0" "succ"] "(fun fO fS n -> if n = 0 then f O () else fS (n-1))".
Extraction insert.
Extraction insertion_sort.
(** val insert : int -> int list -> int list **)

let rec insert a l = match l with
| [] -> a::[]
| x::xs -> if Nat.leb a x then a::l else x::(insert a xs)

(** val insertion_sort : int list -> int list **)

let rec insertion_sort = function
| [] -> []
| x::xs -> insert x (insertion_sort xs)

Haskellの場合

Extraction Language Haskell.

Extract Inductive list => "([])" ["[]" "(:)"].
Extract Inductive bool => "Bool" ["True" "False"].
Extract Inductive nat => Int ["0" "succ"] "(\fO fS n -> if n == 0 then fO () else fS (n-1))".
insert :: Int -> (([]) Int) -> ([]) Int
insert a l =
  case l of {
   [] -> (:) a [];
   (:) x xs ->
    case leb a x of {
     True -> (:) a l;
     False -> (:) x (insert a xs)}}

insertion_sort :: (([]) Int) -> ([]) Int
insertion_sort l =
  case l of {
   [] -> [];
   (:) x xs -> insert x (insertion_sort xs)}

Schemeの場合

Extraction Language Scheme.

Extraction insert.
Extraction insertion_sort.
(define insert (lambdas (a l)
  (match l
     ((Nil) `(Cons ,a ,`(Nil)))
     ((Cons x xs)
       (match (@ leb a x)
          ((True) `(Cons ,a ,l))
          ((False) `(Cons ,x ,(@ insert a xs))))))))

(define insertion_sort (lambda (l)
  (match l
     ((Nil) `(Nil))
     ((Cons x xs) (@ insert x (insertion_sort xs))))))

ファイルへの出力

Extraction Language Ocaml.
Extraction "insertion_sort.ml" insertion_sort.

と入力して proof-general で C-c C-n すると以下のようなファイルが生成された。

module Nat =
 struct
  (** val leb : Int -> Int -> Bool **)

  let rec leb n m =
    (\fO fS n -> if n == 0 then fO () else fS (n-1))
      (fun _ ->
      True)
      (fun n' ->
      (\fO fS n -> if n == 0 then fO () else fS (n-1))
        (fun _ ->
        False)
        (fun m' ->
        leb n' m')
        m)
      n
 end

(** val insert : Int -> Int ([]) -> Int ([]) **)

let rec insert a l = match l with
| [] -> a:[]
| x:xs ->
  (match Nat.leb a x with
   | True -> a:l
   | False -> x:(insert a xs))

(** val insertion_sort : Int ([]) -> Int ([]) **)

let rec insertion_sort = function
| [] -> []
| x:xs -> insert x (insertion_sort xs)
module Nat :
 sig
  val leb : Int -> Int -> Bool
 end

val insert : Int -> Int ([]) -> Int ([])

val insertion_sort : Int ([]) -> Int ([])

lebも作ってくれるのか。 まあないとコードにならないもんな。

証明駆動開発のステップ

  1. まず書こうとしているプログラムがどういう性質をみたすべきかを記述し、
  2. Coq でそれをみたすようなプログラムを書き、
  3. 実際に最初に考えた性質を証明し、
  4. Extraction して他の言語のコードに変換する

感想

形式証明が慣れてないからなのかとても難しかった。
ただ、証明のステップを追うのはとても気持ちよかった。

次は、最近発売された純粋関数型データ構造読むかなって気分。
SML で書かれているらしいから、OCaml に置き換えながら写経するのが楽かな?
それとも付録に Haskell 実装があるらしいので Haskell に置き換えながら写経して、書けたら答え合わせするほうがいいかな。
悩ましい。

プログラミング Coq 証明駆動開発(1)

証明駆動開発入門(1)

何かを読む会 という社内勉強会が発足されました。 読んだ本の内容を共有しよう。 一人で勉強していてもダレるので共有することで無理やり進捗を出そう。 他の人の発表を聞いて読んだ気になろう。 っていう緩めの会です。 途中まで読んで放置していたプログラミング Coq の続きを読んでまとめました。

挿入ソートを証明する。

証明したいことは次の二点。

  • 挿入前と挿入後で要素に変化がないこと(isort_permutation)
  • 挿入後に要素が整列されていること(isort_sorted)

上記を型で示すと以下のようになる。

isort_permutation : forall (l : list nat), Permutation l (insertion_sort l)
isort_sorted      : forall (l : list nat), LocallySorted le (insertion_sort l)

実装

Require Import List.
Require Import Arith.

Fixpoint insert (a : nat) (l : list nat) : list nat :=
  match l with
  | nil => a :: nil
  | x :: xs => if leb a x then a :: l else x :: insert a xs
  end.

Fixpoint insertion_sort (l : list nat) : list nat :=
  match l with
  | nil => nil
  | x :: xs => insert x (insertion_sort xs)
  end.

要素の変化がないこと

あるリストがあるリストと同じ要素で成り立っているのは以下のモジュールで定義されている。

Inductive Permutation : list A -> list A -> Prop :=
  | perm_nil: Permutation [] []
  | perm_skip x l l' : Permutation l l' -> Permutation (x::l) (x::l')
  | perm_swap x y l : Permutation (y::x::l) (x::y::l)
  | perm_trans l l' l'' : Permutation l l' -> Permutation l' l'' -> Permutation l l''.
  1. nilnil は同じ要素から成り立つ
  2. l と l' が同じ要素から成り立つならば x :: l と x :: l' も同じ要素から成り立つ
  3. y :: x :: l と x :: y :: l は同じ要素から成り立つ
  4. (l と l' が同じ要素から成り立ち、l' と l'‘ が同じ要素から成り立つ) ならば l と l’‘ も同じ要素から成り立つ

isort_permutation の証明

isort_permutation の型

forall (l : list nat), Permutation l (insertion_sort l)

帰納法を使う。 l が nil の時は insertion_sort l は nil なので Permutation nil nil となり自明。

帰納法のため、nの場合にあたる仮定は

forall (l : list nat), Permutation xs (insertion_sort xs)

n + 1 に当たる命題は

forall (l : list nat), Permutation x :: xs (insertion_sort x::xs)

となり、

forall (l : list nat), Permutation x :: xs (insert x (insertion_sort xs)

と変形できる。

つまり

forall (l : list nat), Permuation x :: xs (x :: insertion_sort xs)

forall (l : lsit nat), Permutation (x :: insertion_sort xs) (insert x (insertion_sort xs)

を示すことで perm_trans から

forall l l' l'' , Permutation l l' -> Permutation l' l'' -> Permutation l l''
Permutation (x :: xs) (x :: insertion_sort xs) ->
  Permutation (x :: insertion_sort xs) (insert x (insertion_sort xs)) ->
    Permutation (x :: xs) (insert x (insertion_sort xs))

となり、導ける。

A については 仮定と Permutation のコンストラクタ

perm_skip : forall x l l', Permutation l l' -> Permutation (x :: l) (x :: l')

から導ける。

まず B を補題として証明する。

isort_permutaiton の証明は以下。

命令 説明
intros forall などから変数を仮定へ移動する
simpl 簡約
apply 仮定や定理などを適用
destruct 条件分岐しているものなどを subgoal に分ける
induction 帰納法を実施するために subgoal に分ける

どういうふうに証明が進むかは coq ide や proof-general 使って見てください。

Require Import List.
Require Import Arith.
Require Import Sorting.Permutation.
Require Import Sorting.Sorted.

(* isort_permutation *)

Lemma insert_perm : forall (x : nat)(l : list nat), Permutation (x :: l) (insert x l).
  induction l.
  intros.
  simpl.
  apply Permutation_refl.

  intros.
  simpl.
  destruct (leb x a).

  apply Permutation_refl.

  apply perm_trans with (a :: x :: l).
  apply perm_swap.

  apply perm_skip.
  apply IHl.
Qed.

Theorem isort_permutation : forall (l : list nat), Permutation l (insertion_sort l).
  induction l.
  apply perm_nil.
  simpl.
  apply perm_trans with (a :: insertion_sort l).
  apply perm_skip.
  apply IHl.
  apply insert_perm.
Qed.

整列の定義

リスト l が整列されていることはSorting.Sortedモジュールで定義されている.

Induction LocallySorted (A : Type) (R : A -> A -> Prop) : list A :=
  | LSorted_nil : LocallySorted R nil
  | LSorted_cons1 : forall a : A, LocallySorted R (a :: nil)
  | LSorted_consn : forall (a b : A) (l : list A),
    LocallySorted R (b :: l) ->
      R a b -> LocallySorted R (a :: b :: l)

上の定義は次のような意味です。 R a b は a < b のようなものです。

  1. nil は整列している
  2. x :: nil は整列している
  3. b :: l が整列しているとき, R a b ならば a :: b :: l は整列している

整列されていることの証明

こちらでも帰納法で考える。 まず l が nil の場合は insertion_sort nil = nil となり、LSorted_nil : LocallySorted le nil から明らか。

LocallySort le (insertion_sort l) -> LocallySort le (insertion_sort (a :: l)) の場合を考える。 LocallySort le (insertion_sort (a ::l) は LocallySort le (insert a (insertion_sort l))と変形できる。 この時、insertion_sort l は仮定より整列しているため、

insert_sorted : forall (a : nat) (l : list a), LocallySort le l -> LocallySorted le (insert a l)

を示すことができれば証明できる。

これを補題として証明をすすめる。

整列の証明

Lemma insert_sorted : forall (a : nat) (l : list nat),
    LocallySorted le l -> LocallySorted le (insert a l).
  induction l.
  constructor.

  intro.
  simpl.
  remember (leb a a0).
  destruct b.

  apply LSorted_consn.
  apply H.
  apply leb_complete.
  congruence.

  inversion H.
  simpl.
  apply LSorted_consn.
  apply LSorted_cons1.
  apply lt_le_weak.
  apply leb_complete_conv.
  congruence.

  subst.
  simpl.
  simpl in IHl.
  remember (leb a b).

  destruct b0.
  apply LSorted_consn.
  apply IHl.
  apply H2.

  apply lt_le_weak.
  apply leb_complete_conv.
  congruence.

  apply LSorted_consn.
  apply IHl.
  apply H2.
  apply H3.
Qed.
Theorem isort_sorted : forall (l : list nat) , LocallySorted le (insertion_sort l).
  induction l.
  constructor.

  simpl.

  apply insert_sorted.
  apply IHl.
Qed.

これで isertion_sort はソートの前後で要素が変わらないことと、ソート後に整列されていることが証明できた。

技術書典2に行ってきた

お昼頃に予定があったので行くか迷っていたが、14時くらいには空いてきたということで技術書典2に行ってきた。

目当ての一つだったインターネットの闇さんのコンパイラの本は既に完売と向かってる最中の電車の中で知る。 Coqに興味があったのでCoqによる定理証明が買えるといいなと思いながら突入。

16時過ぎでもう終わりかけなのになかなか賑わっていた。 案の定、既に完売で何も片付けられているスペースもチラホラと。 Coqによる定理証明のスペースを見つけたので、中身を見させてもらいながらCoqについて色々と教えていただいた。 入門書かと思っていたけど違った。 3部出ているうちの、一番簡単そうな2014年出版のものを買った。 まずは入門して、そして読まねば。

その後ぶらぶらしていたら、インターネットの闇さんのスペースを見つけたので、見本を見させてもらいながら色々話した。 見本に載っているOCamlのコードはとても読みやすかったので、電子書籍版を期待していると伝え、またフラフラと。

移動してすぐにFortranオブジェクト指向プログラミングをするという尖ったことをしているところで声をかけられて Fortran の話を聞いた。 Fortran については、科学技術計算で主に使用されていることと、現在使われているプログラミング言語の中で最も古い言語の一つってことくらいしか知らなかったのでおもしろかった。 結局バグを減らしたかったり、大学みたいに人が入れ替わる環境だと既存のコードがすぐにレガシーになるので、可読性を高めたいということだった。 Fortran自体にオブジェクト指向が導入されたのはFortran2003かららしいが、ユーザが少ないらしく最適化が後回しにされたりすることもあるらしい。 自分が実際に触ることはないだろうけど、知らない言語の話を聞くのは面白かった。 入門部分も書かれているという第一部を買った。 速習する部分があったので、そこくらいは読んでおきたい。

出不精なので秋葉原までの遠出はつらかったが、普段聞けないことを色々聞けてよかった。

Pathname#joinの不思議な挙動

空のPathname同士をjoinした時に期待と違う挙動があった。

 $ ruby -v
ruby 2.3.3p222 (2016-11-21 revision 56859) [x86_64-darwin16]

期待していたのは次の動作。

path = Pathname.new('')         # => #<Pathname:>
path.join(path)                 # => #<Pathname:>

でも実際はこうなっていた。

path = Pathname.new('')         # => #<Pathname:>
path.join(path)                 # => #<Pathname:.>

空のPathnameと空のPathnameをjoinしてるんだから空のPathnameが欲しかったのに、 . がどこからか出てきてる。
なぜこうなっているんだろう。

剰余を使わないFizzBuzz

先日ESMで開かれたよちよち.hsに参加しました.
そこで剰余を使わずにzip3と無限リストを使ってFizzBuzzを書く話があったので書いてみました.

fizzbuzz = map fizzbuzz' $ zip3 [1..] (cycle ["","","Fizz"]) (cycle ["", "", "", "","Buzz"])
  where fizzbuzz' (_, "Fizz", "Buzz") = "FizzBuzz"
        fizzbuzz' (_, "Fizz", _) = "Fizz"
        fizzbuzz' (_, _, "Buzz") = "Buzz"
        fizzbuzz' (n, _, _) = show n
*Main> take 100 fizzbuzz
["1","2","Fizz","4","Buzz","Fizz","7","8","Fizz","Buzz","11","Fizz","13","14","FizzBuzz","16","17","Fizz","19","Buzz","Fizz","22","23","Fizz","Buzz","26","Fizz","28","29","FizzBuzz","31","32","Fizz","34","Buzz","Fizz","37","38","Fizz","Buzz","41","Fizz","43","44","FizzBuzz","46","47","Fizz","49","Buzz","Fizz","52","53","Fizz","Buzz","56","Fizz","58","59","FizzBuzz","61","62","Fizz","64","Buzz","Fizz","67","68","Fizz","Buzz","71","Fizz","73","74","FizzBuzz","76","77","Fizz","79","Buzz","Fizz","82","83","Fizz","Buzz","86","Fizz","88","89","FizzBuzz","91","92","Fizz","94","Buzz","Fizz","97","98","Fizz","Buzz"]

無限リストが扱いやすくていいですね.
こういう書き方もあったとは