不安全的强制和更高效的Agda代码(-ftrust-me-im-agda)

Question

在Agda邮件列表中,Conor McBride问道:

有没有办法像假定的那样掌握行动

   trustFromJust :: Maybe x -> x

如果没有任何东西,它实际上并没有检查Just and Goes Wrong(在Milner的意义上)？

Agda可能会证明Maybe a == Just1 a,并且可以消除sum类型的中间构造函数.

我可以想到使用unsafeCoerce#或unpackClosure#的方法,但其他人是否有想法？

import GHC.Prim

trustFromJust :: Maybe x -> x
trustFromJust x = y
    where Just1 y = unsafeCoerce# x

data Just1 a = Just1 a

虽然这个段错误(单个构造函数类型可以避免一些闭包开销).核心看起来不错:

main2 =
  case (Data.Maybe.Just @ Type.Integer main3)
       `cast`
       (CoUnsafe
         (Data.Maybe.Maybe Type.Integer)
         (Just1 Type.Integer)
               :: Data.Maybe.Maybe Type.Integer
                    ~
                  Just1 Type.Integer)
  of _ { Just1 y_aeb ->
  $wshowsPrec 0 y_aeb ([] @ Char)

Answer 1

由于这是一个研究问题,我们有一些可能的前进方法,但它们都归结为:

• 玩技巧扭转了Maybe的标记位