Re: [Haskell-cafe] Does the constraints library give (a :- b) -> Dict (a |- b)?

1 Dec 2023


      On Fri, Dec 01, 2023 at 03:03:17PM +0000, Li-yao Xia wrote:
...
There is an issue with bottoms/nontermination (which I don't see
mentioned in those threads).
Yes, but can we resolve it by simply removing the possibility for
bottom, e.g. by making Dict unlifted?  The below code seems to be fine
for example (it prints "fake dictionary"), and that only relies on
making sure that the Dict# is sufficiently evaluated.

Tom


unImply# :: forall c d. Dict# (Implies c d) -> Dict# c -> Dict# d
unImply# (Dict# f) (Dict# c) = Dict# (unsafeCoerce f c)

toDict :: Dict# c -> Dict c
toDict !d = applyDict# ((:-) Dict) d

fake# :: Dict# Unsat
fake# =
  unImply#
    (apDict# (\_ -> error "fake dictionary") :: Dict# (Implies ()
    Unsat))
    (toDict# Dict)

main :: IO ()
main = do
  putStrLn "Hi"
  applyDict uncallable (toDict fake#)
  putStrLn "Bye"

Re: [Haskell-cafe] Does the constraints library give (a :- b) -> Dict (a |- b)?

Tom Ellis