Is there a way to 'restrict' elm function f : A -> Maybe B into f0 : ProperA -> B without using Debug.todo?

Question

A function f: A -> Maybe B. is given.

Then a function isProper : A -> Bool can be defined by

isProper a =
    case f a of
        Just _ ->
            True

        Nothing ->
            False

And let there is a type wrapping A,

type alias ProperA =
    ProperA A

which can be only generated by the function

fromA: A -> Maybe ProperA
fromA a =
    if isProper a then
        Just (ProperA a)
    else
        Nothing

What I want to get is the function f0 : ProperA -> B, which

Just (f0 (ProperA a)) == f a

is True. (f0 doesn't have to exactly be in that form; I want to get B type value from A-like type value without using case expression)

This issue happens when I try to use functions like String.uncons when I already know that the string is ensured to be nonempty, since the string is constructed with functions like String.cons.

I faced such problems multiple times, so I want a general solution.

Simply, I have thought of

f0 (ProperA a) =
    case (f a) of
        Just b ->
            b
        Nothing ->
            Debug.todo "No way!"

But is there any better way than using Debug.todo for the case that would never happen? Or, is there any other way to solve the problem without generating such function? (The core problem is to make impossible states impossible.)

Optionally, how can be this problem solved in other functional languages?

Answer 1

You asked for a type that lets you encode in the type system that something is true so that your function can always work and you don't need a Maybe.

A good way

The general way of making impossible states impossible is to roll your own (sum) types that represent all the possible states.

If you want a string that definitely has a first character, you could define

type NonEmptyString = NES Char String

toString : NonEmptyString -> String
toString NES c s =
    String.cons c s

You can do similarly for lists etc, and as @naïm-favier says, there are plenty of packages that do the non-empty thing for you.

A not-so-good way

The idea with Debug.todo is unsatisfactory, and you could make it better or worse depending on your viewpoint by just using a dummy value for your target type, like

unsafeHead : ProperA String -> Char
unsafeHead (ProperA string) = 
    case String.uncons string of
        Just (h,_) -> 
            h

        Nothing ->
            '∄'

If you make ProperA into an opaque type (elm-radio episode - don't expose the type constructors, just the fromA functions), then the '∄' answer can never occur.

A better way

You seem to be trying to make general solutions to general problems, something programmers are often keen to do. But the lesson of Making Impossible States Impossible isn't to write libraries for subtyping! It's to make domain-specific, problem-specific data types. Types like

 type Size = Standard | Narrow

 type User = NotLoggedIn | LoggedIn Key Profile | SuperUser Key Powers

Move away from using general types and make it specific to your problem. You can add variants later. You can deal with cases specific to your problems.

More generally: ungeneralise.

Ungeneralise! Make your solutions specific to the problem you're solving. It's so super cheap in elm to make new data types that you should be doing it all the time. If you've made a problem-specific data type it will be super easy to change it later. Trust me on this. Maintaining your problem-specific elm code is a dream compared to maintaining other code bases. If you've made an over-generalised data type, you'll be stuck balancing the theoretical needs of your library against the actual needs of your project, and stuck bending the general library to your specific problem's needs. Better to make a problem-specific data type and ditch the premature future-proofing.

(I wish I could make my advice more specific to your problem, but I only have one example of what you're trying to do, but this is great general elm advice.)