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
在某些情況下，使用實際爲此類事物設計的語言更實際一些...... –