15
如果Reverse :: [k] -> [k]是一个类型家族，那么Haskell不能告诉(Reverse (Reverse xs)) ~ xs。有没有办法让类型系统知道这个没有任何运行成本？通知Haskell'（Reverse（Reverse xs））〜xs`
我很想试用unsafeCoerce，但这似乎是一种耻辱。据我所知，以影响GHC的~行为
A
回答
1
的唯一方法是实际构建的a :~: b实例（或类似的，重要的是要构建一个“证明”这对typechecker的术语），然后模式匹配Refl构造函数，这将需要在运行时评估证明见证。我的理解是，GHC中依赖类型的当前设计仍然需要运行所有类型相等的证明。然而，人们可以使用GHC的重写规则，在类型检查之后，用非常低成本的功能（例如unsafeCoerce Refl :: Reverse (Reverse a) :~: a）替换证明证人，这将使得评估成本非常低，但仍然安全（因为证明证人已经被查证，表明如果它终止，它会产生一个正确的证据）。有关依赖打字在Haskell当前状态
了解更多信息可以在这里找到：https://typesandkinds.wordpress.com/2016/07/24/dependent-types-in-haskell-progress-report/
相关问题
- 1. Haskell - 如何将最大（xs ++ map（x +）xs）转换为max（最大xs）（x +最大xs）
- 2. Reverse slideToggle
- 3. Reverse MemoryStream.ToArray（）
- 4. Reverse requirements.txt
- 5. Reverse animateWithDuration
- 6. startAnimatingWithImagesInRange reverse
- 7. Reverse Streamreader
- 8. geocode reverse
- 9. reverse htmlspecialchars
- 10. Reverse factorial
- 11. reverse C++ array
- 12. AVPlayer Reverse Playback
- 13. NSoperation reverse dependencies
- 14. ModelMultipleChoiceField和reverse（）
- 15. php reverse imagecreatefromstring
- 16. Android Reverse Geocode
- 17. Switch Statement Reverse
- 18. Django HttpResponseRedirect和reverse（）
- 19. mysql substring_index reverse
- 20. Postgres“reverse count（*）”（unnest？）
- 21. “Reverse GROUP_CONCAT”in MySQL？
- 22. Reverse Ajax + JSP-Servlet
- 23. Reverse Ajax + Spring MVC
- 24. angularslideables reverse effect
- 25. reverse colortransform alpha AS3
- 26. reverse serialize（）-jquery
- 27. Phonegap - Reverse ajax
- 28. Reverse FloatToStrF结果
- 29. git reverse cherrypick
- 30. AS3 Netstream Reverse
AFAICS，没办法的事，目前。这就是为什么我希望有一天能够看到GHC集成一个终止检查器，并且当'T'只有一个无参数构造函数时，内部优化任何可证实终止'x :: T'到'x = unsafeCoerce（） ：〜：'确实）。仍然需要通过归纳来编写证明，但至少不会引入运行时惩罚。 – chi
在某些情况下，使用实际为此类事物设计的语言更实际一些...... –