作者CoNsTaR ((const *))
看板PLT
標題[問題] Agda 的 instance resolution
時間Sun Apr 26 12:52:05 2020
最近這裡好像比較熱鬧，希望有大大能看到我的問題 orz
廢話有點多，如果想直接看問題的話請直接拉到最下面
假設有一個 Id : String → Set，用來表示 Minecraft 中的各種不同物品
data Id : String → Set where
id : (rawId : String) → Id rawId
對於一種物品我們須要知道的事只有三個，名字、物品欄中的可堆疊數量、是否能在創造
模式物品欄中直接獲得
record Item {rawId : String} (_ : Id rawId) : Set where
field
displayName : Id rawId → String
stacks : Id rawId → Fin 65
obtainable : Bool
開始新增物品種類到 Minecraft 世界中
instance
用 "minecraft:stone" 建立的 Id 當作石頭的 ID，石頭可以堆疊 64 個，可從創造模式
物品欄直接活獲得
Stone : Item (id "minecraft:stone")
Stone =
record {
displayName = "Stone";
stacks = # 64;
obtainable = true
}
盔甲座 ID 是 "minecraft:armor_stand"，可堆疊 16 個，可以從創造模式物品欄直接獲
得
ArmorStand : Item (Id "minecraft:armor_stand")
ArmorStand =
record {
displayName = "Armor Stand";
stacks = # 16;
obtainable = true
}
-- Normal form 是 "Stone"
stoneDisplayName : String
stoneDisplayName = displayName (Id "minecraft:stone")
-- Normal form 是 "Armor Stand"
armorStandDisplayName : String
armorStandDisplayName = displayName (Id "minecraft:armor_stand")
以上程式都還沒有問題，我想問的是下面這個
itemDisplayName : String → String
itemDisplayName rawId = displayName (Id rawId)
會報錯，因為不是所有 rawId 都有一個 Item 的 instance
我想問的是，在 Agda 裡要怎麼保證所有用來呼叫 itemDisplayName 的 String 都有一
個 Item 的 instance？
(is it even possible? what should I be searching for?)
例如有什麼辦法可以弄到一個 proof 之類的，然後編譯器就不會報錯了嗎？
謝謝！
（目前想到的方法就只有枚舉所有 instance 來 pattern matching，但顯然在 instance
數量很多的情況下不是什麼好方法）
--
※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 174.112.166.163 (加拿大)
※ 文章網址: https://webptt.com/m.aspx?n=bbs/PLT/M.1587876727.A.FB6.html
※ 編輯: CoNsTaR (174.112.166.163 加拿大), 04/27/2020 16:22:39
1F：推 stopcrying: 來發正念召喚看看 banacorn 或 petercommand ...04/27 20:56
3F：→ stopcrying: ptrcmd> 就..直接把 instance 傳進去阿..XD04/27 22:36
4F：→ CoNsTaR: 感謝回答！ 抱歉沒講清楚，rawId 有可能是 runtime 的輸04/27 23:43
5F：→ CoNsTaR: 入04/27 23:43
6F：→ CoNsTaR: 如果把 itemDisplayName 的 type 改成 String -> Maybe S04/27 23:43
7F：→ CoNsTaR: tring 的話有解嗎 @@04/27 23:43
8F：→ CoNsTaR: 主要就是希望保留 instance resolution，而且須要某種方 04/27 23:49
9F：→ CoNsTaR: 法在 runtime 知道 resolution 成功與否（雖然說 resolut04/27 23:49
10F：→ CoNsTaR: ion 是在 compile time orz...）04/27 23:49
11F：→ CoNsTaR: 是不是須要 reflection 啊04/27 23:50
12F：→ suhorng: 不知道為什麼想到 type provider. 沒有很懂問題描述XD 05/28 11:35
如果是 idris 的話應該可以用 type provider 編譯期搜尋所有 Item 的 instance，然
後把搜尋的結果拿去 impl Enum？
我覺得我想要的東西有點像 Idris 的 named implementation，而且要有可以在 runtime
選擇 implementation 的方法
應該可以說是會自動建 impl list 的 ad-hoc polymorphism，每實作一個新的 impl 就
像是往那個 list 裡加東西一樣（如果沒用到 compile time 可以 erase 掉）
我的想法是 type class 其實就是 ad-hoc 的 sum type，所以 type class 有一個 impl
list 就好像 sum type 可以 derive Enum 一樣
回得有點晚，抱歉...
※ 編輯: CoNsTaR (174.112.166.163 加拿大), 08/13/2020 15:06:46
13F：推 xcycl: Agda 的 reflection 只有在 type-checking 階段發生 09/05 10:34