Non-determinism on a set defined by the characteristic function

I'm writing an implementation for a non-deterministic finite state automaton (NFA) which has the goal to accurately convey information about the state set through types, which can be reasoned through type algebra.

The mathematical typing definition of the transition function for an NFA is Q ⨯ (Σ ∪ ε) → P(Q), where Q is the set of states, Σ is the set of symbols, ε is the empty symbol, and P(Q) is the power set of Q.

My current implementation models the transition function as transition :: s -> Maybe a -> [s]. Although this makes use of the List Monad's non-determinism feature, it doesn't convey accurate typing information.

Since a -> b is equivalent to b^a in type algebra, I thought of modelling the power set (which contains 2^|Q| elements) as the characteristic function s -> Bool (2^s), leading to the following type definition for the transition function:

newtype Set s = Set (s -> Bool)
transition :: s -> Maybe a -> Set s

Although I've been able to implement basic operations for sets such as union and intersection, I haven't been able to find a way to do non-deterministic computations on values of type Set s.

I have thought of two approaches:

1. Traversing the domain of the function (s -> Bool)

   • Haskell has no built-in way to do this

2. Following the bind implementation for the List Monad

   • While trying to implement non-determinism the same way as the List Monad, I came across a Stack Overflow question mentioning that implementing the Functor instance for s -> Bool is impossible

So, my question is: is it possible to perform non-deterministic computations on values of a set modelled by the characteristic function, and if it is, how could it be achieved?

I guess you could do something like:

bind :: Universe a => Set a -> (a -> Set b) -> Set b
bind (Set m) f = Set (\b -> any ($b) [bs | a <- universe, m a, let Set bs = f a])

This uses the universe package.

Whether you want to share the value computed by the list comprehension between invocations of the lambda is a memory/time tradeoff that you'll have to think through and/or measure yourself.