Skip to content

Commit

Permalink
shift modules around a bit
Browse files Browse the repository at this point in the history
  • Loading branch information
raehik committed May 11, 2024
1 parent af34110 commit 46055de
Show file tree
Hide file tree
Showing 12 changed files with 300 additions and 265 deletions.
1 change: 0 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,6 @@ handling receives special attention:

* Failures do not short-circuit; if a strengthening is made up of multiple
smaller strengthenings, all are run and any failures collated.
* Failures display the weak and strong (target) type.
* Generic strengthening is scarily verbose: see below for details.

### One definition, strong + weak views
Expand Down
46 changes: 17 additions & 29 deletions TODO.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,36 +2,24 @@
* split into base definitions and orphan instances?
* base needs either, acc, text and prettyprinter

## Failures: Combine it all into one constructor
Same as rerefined, no need to split. It means I have to make earlier decisions
on layout, but that's fine.
## Failures: Pretty refinement failures require exposing `Doc` early
rerefined refinement failures return an ADT, which is something. But we can't
embed that directly in a strengthen failure. We have to prettify to some degree.
But that will force us to perform all the indentation etc. upfront, which is
what we're trying to avoid (since it won't work properly).

## Failures: is Typeable really the right choice?
I probably went with `TypeRep`s for filling out failure detail due to copying
refined's design. With rerefined, I've gone back on that, and I now
don't use `Typeable` at all. That said, is it the right pick here?
Is this even sensible? When a strengthen failure indents, it has semantic
meaning: in this general failure, a more specific failure occurred. Using the
indent also for "in this specific failure, a refinement error occurred" seems
bad, somehow.

* The generics don't use it at all.
* Concrete instances could use an associated type family like `type Name =
"Word32"`.
* And strongweak largely deals in concrete instances.
* We can do the same type-level `Show` stuff that rerefined does.
* And we can embed `PredicateName` for `Refined[1]` instances.
We _could_ fix this by going back on our new design, and making a failure
constructor specifically for refinement failures. But that seems like a big code
smell.

The user will have to fill out a bunch of associated type families when using
strongweak, which sucks. Or maybe we can do a shitty job automatically for
generics? Like we can get the datatype name-- no other info, but that's a good
start lol.
Alternatively, we store `Doc`s instead of `Builder`s. Then we can layout in the
`Strengthen Refined` instance. But that seems wrong, too.

The `Show`ing feels a little weird too, but I think it's just that we get away
with it thanks to having lots of concrete instances. Non-concrete instances
would drop it.

Hmm. Not too sure how `Refined` instances will look. How do we get a `Symbol`
from the `a` in `Refined p a`? We can say "it's some type refined with this
predicate", but we apparently can't tell you the type.

Hold on, we went with type-level show for predicates because we were doing lots
of combination. We do no such thing here. Why don't we just write in the
`TypeRep`s ourselves? Easy for concrete, fine for `Refined`. Apparently not a
problem for decomposing instances either.
Orrrr I know it's stupid, but we could have a `prettyRefineFailure :: E ->
[TBL.Builder]`, where the indents are prepared for us. Then we can add our own
base indent on top. No issue. OK, I guess we stick with the current setup.
6 changes: 3 additions & 3 deletions flake.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

53 changes: 50 additions & 3 deletions src/Strongweak/Generic.hs
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
{-# LANGUAGE UndecidableInstances #-} -- required due to nested constraints

-- | Generic 'strengthen' and 'weaken'.

module Strongweak.Generic
Expand All @@ -13,9 +15,13 @@ module Strongweak.Generic
, GenericallySW(..)
) where

import Strongweak.Generic.Weaken
import Strongweak.Generic.Strengthen
import Strongweak.Generic.Via
import Strongweak.Weaken.Generic
import Strongweak.Strengthen.Generic

import Strongweak.Weaken ( Weaken(Weak, weaken) )
import Strongweak.Strengthen ( Strengthen(strengthen) )
import GHC.Generics
import Data.Kind ( Type )

{- $generic-derivation-compatibility
Expand All @@ -41,3 +47,44 @@ types: for the datatype, constructors and selectors. GHC will always add this
metadata for you, but manually-derived Generic instances (which are usually a
bad idea) do not require it.
-}

{- | @DerivingVia@ wrapper for strongweak instances.
We can't use 'Generically' conveniently because we need to talk about two data
types, not one -- we would have to do something like @'Generically' ('Tagged' w
s)@, which is ugly. So we instead define our own adorable little "via type"
here!
Use like so:
@
data XYZ (s :: Strength) = XYZ
{ xyz1 :: SW s Word8
, xyz2 :: Word8
, xyz3 :: ()
} deriving stock Generic
deriving via (GenericallySW (XYZ 'Strong) (XYZ 'Weak)) instance Weaken (XYZ 'Strong)
deriving via (GenericallySW (XYZ 'Strong) (XYZ 'Weak)) instance Strengthen (XYZ 'Strong)
@
TODO can't figure out a way around multiple standalone deriving declarations :(
TODO maybe GenericallySW1? but even so instances differ between weaken and
strengthen (weaken needs nothing) so it's kinda better this way. :)
-}

newtype GenericallySW s (w :: Type) = GenericallySW { unGenericallySW :: s }

instance
( Generic s, Generic w
, GWeaken (Rep s) (Rep w)
) => Weaken (GenericallySW s w) where
type Weak (GenericallySW s w) = w
weaken = weakenGeneric . unGenericallySW

instance
( Generic s, Generic w
, GStrengthenD (Rep w) (Rep s)
, Weaken (GenericallySW s w)
) => Strengthen (GenericallySW s w) where
strengthen = fmap GenericallySW . strengthenGeneric
166 changes: 0 additions & 166 deletions src/Strongweak/Generic/Strengthen.hs

This file was deleted.

50 changes: 0 additions & 50 deletions src/Strongweak/Generic/Via.hs

This file was deleted.

5 changes: 2 additions & 3 deletions src/Strongweak/Strengthen.hs
Original file line number Diff line number Diff line change
Expand Up @@ -77,9 +77,8 @@ data StrengthenFailure = StrengthenFailure
{ strengthenFailDetail :: [TBL.Builder]
-- ^ Detail on strengthen failure.
--
-- We use a list here to keep us able to prettify. We could simply concatenate
-- each element with a newline, but pretty layouts might want to apply an
-- indent, so better handle it elsewhere.
-- We use a list here for the cases where you want multiple lines of detail.
-- Separating with a newline would make prettifying later harder, so we delay.

, strengthenFailInner :: [(TBL.Builder, StrengthenFailure)]
-- ^ Indexed.
Expand Down
Loading

0 comments on commit 46055de

Please sign in to comment.