常連

### 実現したいこと

Coq を用いてプログラムの単体テスト自動化をしたい

### 前提

C#、Python、Typescript で開発をしている

### 質問内容
Coq を用いればプログラムの単体テストの自動化をできることを知ったのですが、Coq で検証ができるプログラムは Coq または OCaml で記述されたプログラムに限られるのでしょうか？

Coq によるソフトウェアの品質保証について

Haskell,Clojure,OCamlのうち始めるのにおすすめのものはどれですか？
純粋な関数型言語を学びたいです。
ほかにもあったらよろしくお願いします

Haskell,Clojure,OCamlのうち始めるのにおすすめのものはどれですか？

### 前提・実現したいこと
以下のような数式を表すデータ型expを用意したとき、exp 型の数式の文字列表現を返す関数を作りたい。

 type exp =
| Num of int
| Var of string
| Add of exp * exp
| Mul of exp * exp;;


### 発生している問題・エラーメッセージ


エラーメッセージ
This expression has type exp -> string
       but an expression was expected of type exp

### 該当のソースコード
let rec string_of_exp v = function
| Num n -> string_of_int n
| Var x -> int_of_exp x
| Add (x,y) -> make_sum(string_of_exp (x+y))
| Mul (x,y) -> make_sum(string_of_exp (x*y));;


### 試したこと

型変換が上手くいってないのは分かるのですが、どこがおかしいのかよく分かりません。プログラムを直していただけると幸いです。

Ocamlの型変換について

○前提・実現したいこと
プログラミングの基礎という初心者向けのOcamlの教材でメトロネットワークを作る問題をしていたのですが理解できないところがあります。

駅間リストのデータから情報を取り出す関数　get_ekikan_kyori　を作り、駅名を二つ受け取ってその間の距離を返すというものです。
```
get_ekikan_kyori "茗荷谷" "新大塚" global_ekikan_list
```
で　1.2 を返すなどです。　直接繋がっていない時にはinfinityを返します。
```
type ekikan_t = { 
  kiten  : string; (* 起点 *) 
  shuten : string; (* 終点 *) 
  keiyu  : string; (* 経由路線名 *) 
  kyori  : float;  (* 距離 *) 
  jikan  : int;    (* 所要時間 *) 
} 
let global_ekikan_list = [ 
{kiten="代々木上原"; shuten="代々木公園"; keiyu="千代田線"; kyori=1.0; jikan=2}; 
{kiten="代々木公園"; shuten="明治神宮前"; keiyu="千代田線"; kyori=1.2; jikan=2}; 
{kiten="明治神宮前"; shuten="表参道"; keiyu="千代田線"; kyori=0.9; jikan=2}; 
{kiten="表参道"; shuten="乃木坂"; keiyu="千代田線"; kyori=1.4; jikan=3}; 
{kiten="乃木坂"; shuten="赤坂"; keiyu="千代田線"; kyori=1.1; jikan=2}; 
{kiten="赤坂"; shuten="国会議事堂前"; keiyu="千代田線"; kyori=0.8; jikan=1}; 
{kiten="国会議事堂前"; shuten="霞ヶ関"; keiyu="千代田線"; kyori=0.7; jikan=1};

let rec get_ekikan_kyori eki1 eki2 lst = match lst with
  [] -> infinity
 | {kiten = k; shuten = s; keiyu = y; kyori = r; jikan = j} :: rest ->
    if (eki1 = k && eki2 = s) || (eki1 = s && eki2 = k)
    then r
    else get_ekikan_kyori eki1 eki2 rest

(* テスト *) 
let test1 = get_ekikan_kyori "茗荷谷" "新大塚" global_ekikan_list = 1.2 
let test2 = get_ekikan_kyori "茗荷谷" "池袋" global_ekikan_list = infinity 
let test3 = get_ekikan_kyori "東京" "大手町" global_ekikan_list = 0.6 
```

パターンマッチを使うときは先頭のリストと残りのリストに分けてfirstとrestというパターン変数を使ってアクセスするらしいです。

片方の距離だけなので駅１が始点と終点でif (eki1 = k && eki2 = s) || (eki1 = s && eki2 = k)、
then rで距離を返すのは分かるのですが、なぜelseでrestが出てくるのかがわからないです。
それとパターンマッチでfirstではなく{kiten = k; shuten = s; keiyu = y; kyori = r; jikan = j}を代わりに使ってる理由も教えていただきです。
そもそもなぜ、リストは、first(最初の要素) とrest(その残りの要素)に分けているのでしょうか？

どなたかご存知の方教えていただけたら助かります、、、

[初心者]else文でなぜrestが出てくるのかわからないです　Ocaml

実現したいこと
エラーメッセージの該当箇所を見つける

質問内容
条件分岐に対するデザインレシピを作っていた所、Error : illegal character (\129) と出たのですが、どの文字がダメなのかわかりません。

作ったデザインレシピ

(* 目的:現在の気温ｔが１５以上２５以下かどうかチェックする *)
(* kaiteki : int -> bool *)
let kaiteki t = false

(* テスト *)
let test1 = kaiteki 7 = false 
let test2 = kaiteki 15 = true 
let test3 = kaiteki 20 = true
let test4 = kaiteki 28 = false　

エラーメッセージ
illegal character (\129)

試したこと
目的内の''tと数字''の全半角



ocamlのエラーメッセージについて

### 前提・実現したいこと

Ocamlで、名前を与えたら、自己紹介する文を返す関数を作ったのですがエラーになってしまいます。
Ocamlに詳しい方おりましたら、ご教授お願いします。

### 発生している問題・エラーメッセージ

```
Error: Unbound value aiueo

ひらがな入力すると、
# jikoshokai ���いうえお ;;
Alert deprecated: ISO-Latin1 characters in identifiers
Alert deprecated: ISO-Latin1 characters in identifiers
Alert deprecated: ISO-Latin1 characters in identifiers
Alert deprecated: ISO-Latin1 characters in identifiers
Alert deprecated: ISO-Latin1 characters in identifiers
Error: Illegal character (\129)
```

### 該当のソースコード

```ここに言語名を入力

# let jikoshokai namae = 
    "私の名前は" ^ namae ^ "です。よろしくお願いします。" ;;
val jikoshokai : string -> string = <fun>
# jikoshokai aiueo ;;


```

### 試したこと

①他の給与を計算する関数などはうまくいったので、設定等は大丈夫だと思います。

言語もUTF-8になっていて、インタプリタで文字化け等はしません。
試しに、
＃ "あ" ;;
としたら、
- : string = "あ"

と文字化けせずに返ってきます。

②「Files: Auto Guess Encoding」もオンにしています。
### 補足情報（FW/ツールのバージョンなど）

        OCaml version 4.11.2

「Ocaml」初心者　文字を与えて、文章を返す関数がエラーになる

[[1;4];[2;5];[3;6]]　(これをlistと名付けます)
これを
map関数によって各要素の積を取って，それをList.fold_rightによって総和を取るということをしたいです．

詰まっているのは，map関数を使い方で，上記のように使うために

map (fun x y -> x*y) list

としたのですが，うまく動いてくれません．記述の仕方が間違っているようなのですが，これはどのように書けば正しく動作しますでしょうか．

ocamlによる内積

###実装したい内容
[ ["apple";"grape"] ; ["orange";"apple"] ; ["lemon";"melon";"banana"] ] (=BIG_list)
のような文字列のリストのリストが引数として与えられたときに
[ ("apple",1) ; ("apple",2) ; ("grape", 1) ; ("orange",2); ... ; ("banana",3) ]
のようなリストを返す関数

###現段階で私が考えている実装方法
(1)指定した要素がリスト内に属しているかを返すmember関数を作る
```ocaml
#let rec member string list =
  match list with
  | [] -> false
  | h::t -> (string=h) || member string t;;
```


（2）重複なしの文字列によるリストを生成する
["apple";"grape";"orange";"lemon";"melon";"banana"]　(=ELE_list)
そのためにBIG_listの要素をある入れてこれを作れるような関数を考える
次の応用
```ocaml
# let rec unduplicate a =
match a with
| [] -> []
| h::t -> if member h t then unduplicate t
else h::unduplicate t;;
```
(3)
```ocaml
math BIG_list with
| [] -> []
| h::t -> member string h
```
のような形でELE_listの要素がBIG_list中のリストに含まれているかを確認していく(再帰を用いる)．このときcountなどの変数で，今のhがBIG_list中の何番目かを数え，member関数がtrueならば，そのcountと文字列のタプルを格納する．

###問題点
(2)まではなんとか実装の方法を具体的に組めそうなのですが，(3)はやる内容が複雑で，二重のループを組む必要があるので，そこの具体的な実装が思い浮かびません．

###教えていただきたいこと
現段階の私の方法に具体的な実装，もしくは，新たな実装のアルゴリズム