[問題] Agda 的 instance resolution

[CoNsTaR ((const *))]

最近這裡好像比較熱鬧，希望有大大能看到我的問題 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://www.ptt.cc/bbs/PLT/M.1587876727.A.FB6.html
※ 編輯: CoNsTaR (174.112.166.163 加拿大), 04/27/2020 16:22:39
推 stopcrying: 來發正念召喚看看 banacorn 或 petercommand ...
→ stopcrying: petercommand 說 https://bit.ly/2xc9qDc
→ stopcrying: ptrcmd> 就..直接把 instance 傳進去阿..XD
→ CoNsTaR: 感謝回答！ 抱歉沒講清楚，rawId 有可能是 runtime 的輸
→ CoNsTaR: 入
→ CoNsTaR: 如果把 itemDisplayName 的 type 改成 String -> Maybe S
→ CoNsTaR: tring 的話有解嗎 @@
→ CoNsTaR: 主要就是希望保留 instance resolution，而且須要某種方
→ CoNsTaR: 法在 runtime 知道 resolution 成功與否（雖然說 resolut
→ CoNsTaR: ion 是在 compile time orz...）
→ CoNsTaR: 是不是須要 reflection 啊
→ suhorng: 不知道為什麼想到 type provider. 沒有很懂問題描述XD
如果是 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
推 xcycl: Agda 的 reflection 只有在 type-checking 階段發生