Prove exhaustivity of print function based on a string map in Haskell

Question

When I have an "enum" type, that is, an algebraic data type where none of the cases wrap any other data, I commonly like to project a parser/printer off of a mapping to string, to make sure the parser and printer stay in sync as I change code. For example, in Idris:

data RPS = Rock | Paper | Scissors

Eq RPS where
  Rock == Rock = True
  Paper == Paper = True
  Scissors == Scissors = True
  _ == _ = False

StrMap : List (RPS, String)
StrMap =
  [ (Rock, "rock")
  , (Paper, "paper")
  , (Scissors, "scissors")
  ]

I might implement a print function as follows:

print' : RPS -> Maybe String
print' rps = lookup rps StrMap

The problem is, I don't want a Maybe here. I would like to guarantee at compile-time that I have covered all my cases, just like I could if I had written this function by case-splitting on RPS, where the exhaustivity checker would kick in and I could just have print : RPS -> string. In Idris, I know how to recover this with a proof (don't you just love Idris!):

print_exhaustive : (rps : RPS) -> IsJust (print' rps)
print_exhaustive Rock = ItIsJust
print_exhaustive Paper = ItIsJust
print_exhaustive Scissors = ItIsJust

justGetIt : (m : Maybe a) -> IsJust m -> a
justGetIt (Just y) ItIsJust = y

print : RPS -> String
print rps with (isItJust (print' rps))
  | Yes itIs = justGetIt (print' rps) itIs
  | No itsNot = absurd $ itsNot $ print_exhaustive rps

Now in my opinion this is fantastic. I am able to declare in exactly one place in my code what the correlation between an enum case and its associated string is, and I can have a print function and a parse function both written with it (the parse function is omitted here as not relevant to the question, but is trivial to implement). Not only that, but I have been able to convince the typechecker that my print : RPS -> String signature that I wanted isn't bogus, and have avoided the use of any partial functions! This is how I like to work.

However at work most of my code is in F#, not in Idris, so what I end up doing instead is using FsCheck to quasi-prove exhaustivity with a property-based test. That's not too bad, but

The property-based test isn't collocated with the StrMap; it is in a different assembly. I like to collocate my invariants with what they refer to as much as possible.
You could get further in the build process before encountering a failure if you e.g. added a case and forgot to change the StrMap; if you were just sitting there recompiling, as I often do, you would miss it until you actually ran the tests.
I have to use non-exhaustive functions to implement it, because of the weaker type system. This muddies the clarity of what I'm trying to teach my coworkers; I've been trying to convince them of the glory of total functional programming.

We've just started a new project in Haskell, and I've hit a scenario like this. Of course I can use QuickCheck and fromJust and implement the F# strategy, and that should be fine.

But what I'm wondering is: since Haskell community and ecosystem emphasizes the Curry-Howard correspondence in a way that F#'s community and ecosystem doesn't, and since all kinds of fancy extensions have been added in recent days to enable the use of dependent types, shouldn't I be able to follow my Idris strategy for this instead? Someone told me that I should be able to translate anything I can write in Idris to Haskell without loosing type safety if I turned on enough extensions (and was willing to introduce enough verbosity etc). I don't know whether this is true or not, but if it is true, I would like to know what extensions to turn on, and what kind of code to write, in order to follow my Idris strategy for this in Haskell. Also worthy of note: I could believe that my Idris strategy is not the most simple/elegant way of doing it in that language.

How can I translate this Idris code to Haskell in order to implement print :: RPS -> String without invoking any partial functions?

For a low-tech solution, are you willing to trust the derived Enum and Bounded instances for enum types? Because if yes, you can write print as a straight function, and for parse, use a map you can build via [ (a, print a) | a <- [minBound..maxBound] ] — Cactus
@cactus Hm, hadn't thought about that. I've heard of those typeclasses before, but haven't ever used them (I've written mostly F# and Idris, not so much Haskell, and Idris doesn't have deriving yet, etc...) and so they aren't much on my radar. Care to flesh that out into a full answer? — Keith Pinson
I think you can generate Show and Read instances (or just print and parse functions) with some TH. Not an ideal solution but it may also work with things other than enums. — n. 1.8e9-where's-my-share m.
@n.m. I have read the paper about invertible syntax descriptions actually was able to implement enough of it in F# to generate a parser/printer between CLI arguments and an algebraic data type. They did use Template Haskell. I don't know much about Template Haskell though. My F# version had more boilerplate than theirs. — Keith Pinson
@n.m. however that did require more than template Haskell: they needed accompanying type classes, algebra of syntaxes, etc. Enumerations are the degenerate case where it is much easier though. — Keith Pinson

Cactus Cactus · Accepted Answer · 2018-12-06T06:03:04

If you are willing to trust the derived Enum and Bounded instances for your enum type, then that gives you a way to enumerate your "RPS universe" using [minBound..maxBound]. That means you can start from a total function print :: RPS -> String, and tabulate that to compute parse from it:

print :: RPS -> String

parse :: String -> Maybe RPS
parse = \s -> lookup s tab
  where 
    tab = [(print x, x) | x <- [minBound..maxBound]]

Prove exhaustivity of print function based on a string map in Haskell

1 Answers