Open Issues With HERMIT Shell API - ku-fpg/hermit-shell GitHub Wiki
Overloading
The original HERMIT API provides a relatively minimal set of methods. For convenience's sake, the original HERMIT shell provided an overloaded interface to these methods.
Example:
API method:
alphaLam :: Maybe String -> Rewrite LCore
Shell interface:
alphaLam :: Rewrite LCore
alphaLam :: String -> Rewrite LCore
Question: To Overload or Not to Overload?
See: https://github.com/ku-fpg/hermit-shell/wiki/Variadic-Functions-in-Shell-DSL
Overloading is possible via any of the standard methods (see: http://okmij.org/ftp/Haskell/polyvariadic.html). Alternatively, type families can be used to unify instances over return types in the cases where there are not required arguments to build functional dependencies from:
type family ReturnType i :: * where
ReturnType (a -> r) = ReturnType r
ReturnType r = r
-- Rewrites with an optional string
class ReturnType a ~ Rewrite LCore
=> RewriteWithString a where
rewriteWithString :: Text -> a
instance RewriteWithString (Rewrite LCore) where
rewriteWithString x = Transform $ method x [toJSON (Nothing :: Maybe String)]
instance (IsString a, a ~ String) => RewriteWithString (a -> Rewrite LCore) where
rewriteWithString x str = Transform $ method x [toJSON $ Just str]
alphaLam :: (ReturnType a ~ Rewrite LCore, RewriteWithString a) => a
alphaLam = rewriteWithString "alphaLam"
Problems:
There are two problems related to overloading the interface in the new shell:
-
The use of
OverloadedStrings
creates ambiguous types that defeats the primary purpose of overloading, convenience. For example, isalphaAlt (["a", "b"] :: [String])
really preferable toalphaAltWith ["a", "b"]
? -
Using type classes/families to overload the interface muddies the API documentation. Is seeing a function of type
(ReturnType a ~ Rewrite LCore, RewriteWithString a) => a
and a list of instances like(IsString a, a ~ String) => RewriteWithString (a -> Rewrite LCore)
in Haddock useful at all to the user? Manually documenting each overloaded type is possible, but requires extra work and doesn't work with tools like hoogle.
Current Solution:
Currently we perform no overloading and instead implement interface methods using the following naming convention:
-
X :: Rewrite LCore
- a base rewrite,X
, that takes no arguments. Equivalent to calling API methods with optional arguments using aNothing
value. -
XWith :: a -> Rewrite LCore
- a base rewrite,X
, that takes an argument, i.e. doX
witha
. Equivalent to calling API methods with optional arguments using a value of typeJust a
. -
XAny :: [a] -> Rewrite LCore
- a base rewrite,X
, that takes a list of arguments, i.e. doX
with the firsta
that works. Usually maps directly to an equivalent API method but in most cases is functionally equivalent totryFind XWith
wheretryFind :: MonadPlus m => (a -> m b) -> [a] -> m b
.
Externals
Currently, the definition of externals in the new shell is largely inherited from the old shell. Can this be optimized at all?
Problems:
-
Do we need to continue carrying the documentation for external values? GHC is notoriously bad at compiling modules with large numbers of 'String' constants. If we have no intention of using this documentation, i.e. recreating the help functions from the old shell, then we should really get rid of it; both to help compilation and improve the readability/clarity of
External
instances. -
Does
External
need to be a type family? TheHERMIT.Server.Parser.Transform
module is unwieldy to say the least. A lot of this is due to the multipleExternal
instances being mutually-recursive. HS-Boot files do not support type families at this time, so there is no way to separate these instances into their own modules.
Does External
need to be a type family though? It's included type, R
, only has two cases, functional and non-functional, and is only used to compute the return type for matchExternal
which again has only two cases, the default and a special case for functional external values.
R
is identical to the ReturnType
type family from the example in the Overloading section. Could we split it off as a "utility" type family and reduce External
to just a type class?
HermitName
vs. Name
vs. String
The old HERMIT shell had a variety of newtype
wrappers to HermitName
to differentiate between its various uses, mainly for tab completion purposes.
Similarly, it has a variety of newtype
wrappers to String
, e.g. LemmaName
, for similar reasons.
In the new shell we have done a blanket replacement of these types with a single type: Name
; again, a newtype
wrapper to String
.
We need to figure out if we want to distinguish between these types, or if a single type will do. If we decide on the latter, then I'd suggest using String
to eliminate the need for the OverloadedString
extension.
We also probably want to review the API to see where there are inconsistencies. For example inlineWith
takes a Name
but inlineAny
takes a list of String
s. This is due to their correspondence with inlineMatchingPredR
and inlineNamesR
, respectively.
Composing Rewrites
The HERMIT.Dictionary.Kure
module contains a number of operators designed to compose transformations/rewrites/etc.
It is not immediately apparently how we want to handle these operators and where the composition should be performed (see: https://github.com/ku-fpg/hermit-shell/issues/12).
For now, they are overloaded in the new shell's API:
(<+) :: External (TransformH a b)
=> Transform a b -> Transform a b -> Transform a b
(<+) x y = Transform $ method "<+" [toJSON x, toJSON y]
(>>>) :: External (RewriteH a) => Rewrite a -> Rewrite a -> Rewrite a
(>>>) x y = Transform $ method ">>>" [toJSON x, toJSON y]
There are only two original External
instances for (<+)
, though, despite it being a much more polymorphic primitive combinator of KURE. Maybe this is an indication that we are constraining its use by the server too much?
Transform
s
Overloaded Some commands, such as lhs
, rhs
and both
, have Transform
overloaded in at least one argument but are not fully parametrically polymorphic in that argument. For example, the two types of lhs are:
lhs :: TransformH LCore String -> TransformH LCore String
lhs :: RewriteH LCore -> RewriteH LCore
Here are three possible options:
-
Make the command fully parametrically polymorphic:
lhs :: Transform LCore b -> Transform LCore b
- Pros: Simplicity of use and simple implementation
- Cons: Could potentially prevent important type errors from occurring (I'm not sure whether or not this would be the case though)
- Restrict the type argument using the promoted type-level equality and type-level boolean operations provided by
base
(specifically, fromData.Type.Equality
andData.Type.Bool
):
lhs :: (b == String || b == LCore) ~ 'True
=> Transform LCore b -> Transform LCore b
-
Pros: All potential type errors are definitely caught while remaining as polymorphic as possible (that is, it is exactly as polymorphic as it "should be"). Also, note that type error messages remain normal looking if
lhs
is given something that isn't aTransform
at all (for instance, if it is given aCrumb
as its argument instead of some sort ofTransform
). -
Cons: Error messages are less intuitive if it is given the wrong kind of
Transform
. Here's a sample message:
HERMIT> lhs (undefined :: Transform LCore LCoreTC)
:4:1: Couldn't match type ‘'False’ with ‘'True’ Expected type: 'True Actual type: (LCoreTC == String) || (LCoreTC == LCore) In the expression: lhs (undefined :: Transform LCore LCoreTC) In an equation for ‘it’: it = lhs (undefined :: Transform LCore LCoreTC) ```
The most important content of the error message is on the line that says `Actual type: ...`, while the first two lines only tell you that something strange is going on involving promoted booleans.
- Use separate monomorphic functions for each type.
- Pros: Full type safety with no confusing error messages. Using a common prefix allows GHCIs tab completion to help remember the names (not a pro over the other options, but an important point).
- Cons: Need to come up with new names and differs slightly from the original HERMIT interface.
Currently, we use option 3 with the following naming convention:
lhsT :: Transform LCore String -> Transform LCore String
lhsR :: Rewrite LCore -> Rewrite LCore
and so on for the others.
Another command that has a similar issue is parentOf
(from HERMIT.Dictionary.Local.Case
), which has the types:
parentOf :: TransformH LCore LocalPathH -> TransformH LCore LocalPathH
parentOf :: TransformH LCoreTC LocalPathH -> TransformH LCoreTC LocalPathH
This command is unimplemented at the moment, but the above discussion also applies.