PTT數位生活區 / PLT (程式語言與理論)

[問題] Agda 的 instance resolution

看板PLT (程式語言與理論)作者 ((const *))時間4年前 (2020/04/26 12:52), 3年前編輯推噓2(2推 0噓 11→)
留言13則, 4人參與, 3年前最新討論串1/1
最近這裡好像比較熱鬧，希望有大大能看到我的問題 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
推
04/27 20:56, 4年前 , 1F
來發正念召喚看看 banacorn 或 petercommand ...
04/27 20:56, 1F
→
04/27 22:35, 4年前 , 2F
petercommand 說 https://bit.ly/2xc9qDc
04/27 22:35, 2F
→
04/27 22:36, 4年前 , 3F
ptrcmd> 就..直接把 instance 傳進去阿..XD
04/27 22:36, 3F
→
04/27 23:43, 4年前 , 4F
感謝回答！ 抱歉沒講清楚，rawId 有可能是 runtime 的輸
04/27 23:43, 4F
→
04/27 23:43, 4年前 , 5F
入
04/27 23:43, 5F
→
04/27 23:43, 4年前 , 6F
如果把 itemDisplayName 的 type 改成 String -> Maybe S
04/27 23:43, 6F
→
04/27 23:43, 4年前 , 7F
tring 的話有解嗎 @@
04/27 23:43, 7F
→
04/27 23:49, 4年前 , 8F
主要就是希望保留 instance resolution，而且須要某種方
04/27 23:49, 8F
→
04/27 23:49, 4年前 , 9F
法在 runtime 知道 resolution 成功與否（雖然說 resolut
04/27 23:49, 9F
→
04/27 23:49, 4年前 , 10F
ion 是在 compile time orz...）
04/27 23:49, 10F
→
04/27 23:50, 4年前 , 11F
是不是須要 reflection 啊
04/27 23:50, 11F
→
05/28 11:35, 4年前 , 12F
不知道為什麼想到 type provider. 沒有很懂問題描述XD
05/28 11:35, 12F
如果是 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
推
09/05 10:34, 3年前 , 13F
Agda 的 reflection 只有在 type-checking 階段發生
09/05 10:34, 13F
‣ 更多 CoNsTaR 的文章
文章代碼(AID): #1UfHDt-s (PLT)
PLT 近期熱門文章
更多 近期熱門文章 >>
PTT數位生活區 即時熱門文章
更多 即時熱門文章 >>
‣ 更多 CoNsTaR 的文章
文章代碼(AID): #1UfHDt-s (PLT)