[8.8.1] visible type applications

[matsubara0507]

GHC 8.8.1 のハイライト機能の1つ "visible type applications" について

GHC now supports visible kind applications, as described in GHC proposal #15. This extends the existing visible type applications feature to permit type applications at the type level (e.g., f :: Proxy ('Just @Bool 'True)) in addition to the term level (e.g., g = Just @Bool True).

[matsubara0507]

• 元々は GHC proposal #15
• GHC 8.0.1 に導入された TypeApplication を型レベルに拡張する
• Proposal Issue
• GHC ticket
• Merge Request
• 値(項？)レベル: show (read @Int "5")
• 型レベル: 'Just @Nat (instead of 'Just :: Nat -> Maybe Nat ?)

（正直、面白い例が思い浮かばないな。最近型レベルプログラミングしないし。。。）

[matsubara0507]

面白い例？
https://www.reddit.com/r/haskell/comments/bo0q7h/functorof/enion4l/

（この下でレコメンドされた https://www.reddit.com/r/haskell/comments/e7gopg/new_haskell_phd_thesis_on_backback_foundations/ きになるけどw ）

[matsubara0507]

メモ https://hackmd.io/rldhHG8URyO8Hg16eOkIWA