---
tags: PLT
---

# [FunTh#79][FunTh#79]

在忘記之前貼一下，又怕太 low 所以就不貼聊天室洗版。

今天在 [FunTh#79][FunTh#79] 聽 [Ash Manning][a-manning] 講 [F*][fstar] 和 dependent types 。大意是在 dependent type system 中，會把 type 分成一層一層的，高層的 type 可以從低層的 type 組合出來。

例如：

type vector 'a : nat -> Type =
  | VNil : vector 'a 0
  | VCons : hd:'a
         -> #n:nat
         -> tl:vector 'a n
         -> vector 'a (n + 1)

val head: #a:Type -> #n:pos -> vector a n -> Tot a
let head #a #n v = match v with
  | VCons x xs -> x

邊聽邊注意到 type 放在比較前面的參數，想起之前讀 Haskell 的 typeclass 怎麼轉換時，也把帶著 function 的 dictionary 放在第一個參數，於是才問講者， F* 是否有個 core language ，希望能知道他是怎麼轉換的。

但看來是沒有：

> After verification, F* programs can be extracted to efficient OCaml, F#, C, WASM, or ASM code.

後來又拿這件事問 banacorn 和 ptrcmd ， ptrcmd 說放哪個位置沒差，因為不管放哪邊都可以做個 closure 出來幫它換位置。倒是後面的 type 參數會用到前面的。

想想如果不需要 type checking ，那實務上我想要的語言，只需要在程式設計師組織完一個 graph 後，先在 compile 時把可以 reduce 的部分都 reduce 完，剩下的 graph 再拿去給 interpreter 繼續 reduce ，或是轉變成適合某種 machine 的語言即可。

但在 JavaScript 似乎無法靠簡單的 macro 做到這件事， ptrcmd 在走去捷運的路上提醒說，失去 type 資訊後，變成得手動傳 type 或是 dictionary 。

[FunTh#79]: https://www.facebook.com/events/552539818648063/
[a-manning]: https://github.com/a-manning
[fstar]: https://www.fstar-lang.org/