作者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/cn.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