You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
t = covers $ \(Just True) -> Just True
f = covers $ \(Just False) -> Just False
listMaybeBools :: [Maybe Bool]
listMaybeBools = $$(surjective
[||... [ t
, f
]
||])
Thanks to referential transparency, such a substitution is valid in any Haskell program... except this one, because surjective is a macro and it looks at the syntax of the code it checks, not the semantics. Unfortunately, t is only semantically equal to covers $ \(Just True) -> Just True, it is not syntactically identical.
So, would it be possible to support this syntax? I think it would! Macros can lookup identifiers, so surjective could lookup each identifier in the code it is checking, and if the definition of the identifier is a literal call to covers, surjective could act as if it has seen that call directly.
The obvious problem with this approach is that it would only support one level of indirection. If we were to write this instead:
t' = covers $ \(Just True) -> Just True
f' = covers $ \(Just False) -> Just False
t = t'
f = f'
listMaybeBools :: [Maybe Bool]
listMaybeBools = $$(surjective
[||... [ t
, f
]
||])
Then it wouldn't work, for the same reason as before: surjective would lookup t, and while its definition, t', is semantically equal to covers $ \(Just True) -> Just True, it isn't syntactically identical. We could add yet another special case, but then what about (t, f) = (t', f')? Or t = head [t', f']?
Eventually we have to draw the line, otherwise we'll end up writing a Haskell interpreter. I think "a literal call to covers" is the right stopping point, because it allows the definition of t to be moved outside of surjective's scope, making the syntax lighter. Then if we really need to compute t from some more complex expression, we can always use TH to produce a literal call to covers.
The text was updated successfully, but these errors were encountered:
There is an alternative (though I'm not sure how much I like it). Sometimes the solution is to return to the object level: covers is a TH function which takes a lambda :: a -> aand produces a ([Pattern], a), or a Writer [Pattern] a, or some newtype thereof; surjective accumulates those values and produces the pattern match warning.
Another idea: an indicator for explicitly propagating covers (I'm thinking a bit analogous to Python's yield from).
The current API is very noisy:
@rpglover64 suggested a nicer, less noisy API:
Thanks to referential transparency, such a substitution is valid in any Haskell program... except this one, because
surjective
is a macro and it looks at the syntax of the code it checks, not the semantics. Unfortunately,t
is only semantically equal tocovers $ \(Just True) -> Just True
, it is not syntactically identical.So, would it be possible to support this syntax? I think it would! Macros can lookup identifiers, so
surjective
could lookup each identifier in the code it is checking, and if the definition of the identifier is a literal call tocovers
,surjective
could act as if it has seen that call directly.The obvious problem with this approach is that it would only support one level of indirection. If we were to write this instead:
Then it wouldn't work, for the same reason as before:
surjective
would lookupt
, and while its definition,t'
, is semantically equal tocovers $ \(Just True) -> Just True
, it isn't syntactically identical. We could add yet another special case, but then what about(t, f) = (t', f')
? Ort = head [t', f']
?Eventually we have to draw the line, otherwise we'll end up writing a Haskell interpreter. I think "a literal call to
covers
" is the right stopping point, because it allows the definition oft
to be moved outside ofsurjective
's scope, making the syntax lighter. Then if we really need to computet
from some more complex expression, we can always use TH to produce a literal call tocovers
.The text was updated successfully, but these errors were encountered: