Open gergoerdi opened 3 years ago
Some code archeology doesn't explain whether the above approach was tried but rendered unsatisfactory type inference results. Perhaps @blaxill can tell us whether he tried the above approach before submitting the original PR for the Signal.Delayed.Bundle
module?
I don't see any immediate reason not to do it.
Just a heads up, the various bundle
and unbundle
primitives are currently hardcoded in the compiler:
So if we go through with this, it's probably easiest to have the instances of DSignal
be implemented like ~coerce . bundle @(Signal dom) @a . coerce
.
One issue I've realized is that "do-nothing" instances can cause problems with other instances, if their shape is sufficiently similar.
In concrete terms, if we have Bundle (Vec n a)
and Bundle (Maybe a)
, with the former doing actual unbundling and the latter being id
, then we have
type Unbundled f (Maybe a) = f (Maybe a)
type Unbundled f (Vec n a) = Vec n (f a)
And these are sadly overlapping, because what about Vec n (Maybe a)
?
Type family equations violate injectivity annotation:
Unbundled f (Vec n a) = Vec n (f a)
Unbundled f (Maybe a) = f (Maybe a)
If we had proper fundeps for tyfams, maybe res f -> a
would be good enough both to allow these instances and also to make inference work, but it's hard to test this hypothesis without support in GHC...
Some code archeology doesn't explain whether the above approach was tried but rendered unsatisfactory type inference results. Perhaps @blaxill can tell us whether he tried the above approach before submitting the original PR for the
Signal.Delayed.Bundle
module?
No, I don't think I tried- I was learning Haskell and consolidating them was beyond me at the time.
@gergoerdi I tried going for a full MPTC+FD version of Bundle
without TF:
class BundleX a f res | res f -> a where
bundleX :: res -> f a
default bundleX :: res ~ f a => res -> f a
bundleX = id
unbundleX :: f a -> res
default unbundleX :: res ~ f a => f a -> res
unbundleX = id
instance BundleX Bool f (f Bool)
instance Applicative f => BundleX (a, b) f (f a, f b) where
bundleX (x, y) = (,) <$> x <*> y
unbundleX xy = (fst <$> xy, snd <$> xy)
instance Applicative f => BundleX (a, b, c) f (f a, f b, f c) where
bundleX (x, y, z) = (,,) <$> x <*> y <*> z
unbundleX xyz = ((\(x,_,_)->x) <$> xyz, (\(_,y,_)->y) <$> xyz, (\(_,_,z)->z) <$> xyz)
instance (KnownNat n, Applicative f, Traversable f) => BundleX (Vec n a) f (Vec n (f a)) where
bundleX = traverse# id
unbundleX = sequenceA . fmap lazyV
instance BundleX (Maybe a) f (f (Maybe a))
It started out alright, until I hit this snag:
mealyB
:: ( HiddenClockResetEnable dom
, NFDataX s
, BundleX i (Signal dom) iRes
, BundleX o (Signal dom) oRes)
=> (s -> i -> (s,o))
-- ^ Transfer function in mealy machine form: @state -> input -> (newstate,output)@
-> s
-- ^ Initial state
-> (iRes -> oRes)
-- ^ Synchronous sequential function with input and output matching that
-- of the mealy machine
mealyB = hideClockResetEnable E.mealyB
{-# INLINE mealyB #-}
where GHC started throwing:
src/Clash/Prelude/Mealy.hs:120:6: error:
• Could not deduce: (GHC.Classes.IP
(GHC.TypeLits.AppendSymbol dom0 "_clk") (Clock dom0),
GHC.Classes.IP
(GHC.TypeLits.AppendSymbol dom0 "_rst") (Reset dom0),
GHC.Classes.IP
(GHC.TypeLits.AppendSymbol dom0 "_en") (Enable dom0))
from the context: (HiddenClockResetEnable dom, NFDataX s,
BundleX i (Signal dom) iRes, BundleX o (Signal dom) oRes)
bound by the type signature for:
mealyB :: forall (dom :: GHC.Types.Symbol) s i iRes o oRes.
(HiddenClockResetEnable dom, NFDataX s,
BundleX i (Signal dom) iRes, BundleX o (Signal dom) oRes) =>
(s -> i -> (s, o)) -> s -> iRes -> oRes
at src/Clash/Prelude/Mealy.hs:(120,6)-(128,19)
• In the ambiguity check for ‘mealyB’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
mealyB :: (HiddenClockResetEnable dom,
NFDataX s,
BundleX i (Signal dom) iRes,
BundleX o (Signal dom) oRes) =>
(s -> i -> (s, o)) -> s -> (iRes -> oRes)
|
120 | :: ( HiddenClockResetEnable dom
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
which makes sense, since there's nothing to the RHS of =>
that ties down the dom
type variable. And adding a proxy argument to tie down dom
defeats the point of having the IPs for clock/reset/enable to begin with.
So yeah... no win so far.
We can join our two ideas to something that might work! I think your idea of using MPTCs to work around generalized fundeps missing from tyfams is a good one, you just have to get the fundeps right -- including the implicit one that was in the original associated tyfam, since there you always have lhs -> rhs
.
I've tried the following definition:
class Bundle a f res | f a -> res, f res -> a where
bundle :: (Applicative f) => res -> f a
default bundle :: (Applicative f, res ~ f a) => res -> f a
bundle = id
unbundle :: (Traversable f) => f a -> res
default unbundle :: (Traversable f, res ~ f a) => f a -> res
unbundle = id
With the following sigil instances:
instance Bundle Bit f (f Bit) where
instance Bundle (a, b) f (f a, f b) where
bundle (x, y) = (,) <$> x <*> y
unbundle xy = (fst <$> xy, snd <$> xy)
instance (KnownNat n) => Bundle (Vec n a) f (Vec n (f a)) where
bundle = traverse# id
unbundle = sequenceA . fmap lazyV
instance Bundle (Maybe a) f (f (Maybe a)) where
No coverage conflict here!
This chain of definitions works:
mealyB
:: (HiddenClockResetEnable dom)
=> (Bundle i (Signal dom) i', Bundle o (Signal dom) o')
=> (NFDataX s)
=> (s -> i -> (s,o))
-> s
-> (i' -> o')
mealyB = hideClockResetEnable mealyBE
mealyBE
:: (Bundle i (Signal dom) i', Bundle o (Signal dom) o')
=> (NFDataX s)
=> Clock dom
-> Reset dom
-> Enable dom
-> (s -> i -> (s,o))
-> s
-> (i' -> o')
mealyBE = unbundle . mealyE clk rst en f s0 . bundle
mealyE
:: (NFDataX s)
=> Clock dom
-> Reset dom
-> Enable dom
-> (s -> i -> (s,o))
-> s
-> (Signal dom i -> Signal dom o)
mealyE = undefined
Seems usable, e.g.:
foo :: (HiddenClockResetEnable dom) => (Signal dom Int, Signal dom Int) -> (Signal dom Int, Signal dom Int)
foo = mealyB minMax (0, 0)
where
minMax :: (Int, Int) -> (Int, Int) -> ((Int, Int), (Int, Int))
minMax (x, y) (minX, maxY) = ((x + maxY, y + minX), (min x minX, max y maxY))
We might just have cracked this!
(I wish we could write f -> (a <-> res)
as a fundep)
Note that my proposed code above is not as generic as yours, since it requires f
to be Applicative
/ Traversable
even for the trivial instances. I don't have an opinion on whether this is better or not than moving these constraints to individual instances. For completeness's sake, here's a version with constraints on instances:
class Bundle a f res | f a -> res, f res -> a where
bundle :: res -> f a
default bundle :: (res ~ f a) => res -> f a
bundle = id
unbundle :: f a -> res
default unbundle :: (res ~ f a) => f a -> res
unbundle = id
instance Bundle Bit f (f Bit) where
instance (Applicative f) => Bundle (a, b) f (f a, f b) where
bundle (x, y) = (,) <$> x <*> y
unbundle xy = (fst <$> xy, snd <$> xy)
instance (KnownNat n, Applicative f, Traversable f) => Bundle (Vec n a) f (Vec n (f a)) where
bundle = traverse# id
unbundle = sequenceA . fmap lazyV
instance Bundle (Maybe a) f (f (Maybe a)) where
What version of GHC are you using? I changed to:
class BundleX a f res | f a -> res, f res -> a where
bundleX :: Applicative f => res -> f a
default bundleX :: (Applicative f, res ~ f a) => res -> f a
bundleX = id
unbundleX :: Traversable f => f a -> res
default unbundleX :: (Traversable f, res ~ f a) => f a -> res
unbundleX = id
instance (Applicative f, Traversable f) => BundleX Bit f (f Bit) where
instance (Applicative f) => BundleX (a, b) f (f a, f b) where
bundleX (x, y) = (,) <$> x <*> y
unbundleX xy = (fst <$> xy, snd <$> xy)
instance (Applicative f) => BundleX (a, b, c) f (f a, f b, f c) where
bundleX (x, y, z) = (,,) <$> x <*> y <*> z
unbundleX xyz = ((\(x,_,_)->x) <$> xyz, (\(_,y,_)->y) <$> xyz, (\(_,_,z)->z) <$> xyz)
instance (KnownNat n, Applicative f, Traversable f) => BundleX (Vec n a) f (Vec n (f a)) where
bundleX = traverse# id
unbundleX = sequenceA . fmap lazyV
instance (Applicative f, Traversable f) => BundleX (Maybe a) f (f (Maybe a)) where
but for:
mealyB
:: ( HiddenClockResetEnable dom
, NFDataX s
, BundleX i (Signal dom) i'
, BundleX o (Signal dom) o')
=> (s -> i -> (s,o))
-- ^ Transfer function in mealy machine form: @state -> input -> (newstate,output)@
-> s
-- ^ Initial state
-> (i' -> o')
-- ^ Synchronous sequential function with input and output matching that
-- of the mealy machine
mealyB = hideClockResetEnable E.mealyB
{-# INLINE mealyB #-}
I still get the following on GHC 8.10.4:
[102 of 107] Compiling Clash.Prelude.Mealy ( src/Clash/Prelude/Mealy.hs, interpreted )
src/Clash/Prelude/Mealy.hs:120:6: error:
• Could not deduce: (GHC.Classes.IP
(GHC.TypeLits.AppendSymbol dom0 "_clk") (Clock dom0),
GHC.Classes.IP
(GHC.TypeLits.AppendSymbol dom0 "_rst") (Reset dom0),
GHC.Classes.IP
(GHC.TypeLits.AppendSymbol dom0 "_en") (Enable dom0))
from the context: (HiddenClockResetEnable dom, NFDataX s,
BundleX i (Signal dom) i', BundleX o (Signal dom) o')
bound by the type signature for:
mealyB :: forall (dom :: GHC.Types.Symbol) s i i' o o'.
(HiddenClockResetEnable dom, NFDataX s, BundleX i (Signal dom) i',
BundleX o (Signal dom) o') =>
(s -> i -> (s, o)) -> s -> i' -> o'
at src/Clash/Prelude/Mealy.hs:(120,6)-(128,15)
• In the ambiguity check for ‘mealyB’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
mealyB :: (HiddenClockResetEnable dom,
NFDataX s,
BundleX i (Signal dom) i',
BundleX o (Signal dom) o') =>
(s -> i -> (s, o)) -> s -> (i' -> o')
|
120 | :: ( HiddenClockResetEnable dom
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
src/Clash/Prelude/Mealy.hs:120:6: error:
• Could not deduce (KnownDomain dom0)
from the context: (HiddenClockResetEnable dom, NFDataX s,
BundleX i (Signal dom) i', BundleX o (Signal dom) o')
bound by the type signature for:
mealyB :: forall (dom :: GHC.Types.Symbol) s i i' o o'.
(HiddenClockResetEnable dom, NFDataX s, BundleX i (Signal dom) i',
BundleX o (Signal dom) o') =>
(s -> i -> (s, o)) -> s -> i' -> o'
at src/Clash/Prelude/Mealy.hs:(120,6)-(128,15)
The type variable ‘dom0’ is ambiguous
• In the ambiguity check for ‘mealyB’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
mealyB :: (HiddenClockResetEnable dom,
NFDataX s,
BundleX i (Signal dom) i',
BundleX o (Signal dom) o') =>
(s -> i -> (s, o)) -> s -> (i' -> o')
|
120 | :: ( HiddenClockResetEnable dom
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
I tested it with the following Stack resolver:
name: clash-HEAD
resolver: lts-16.21
packages:
- github: clash-lang/clash-compiler
commit: fb903e0b227045e387d5df6ed83009948c403d33
subdirs:
- clash-ghc
- clash-prelude
- clash-lib
- ghc-typelits-knownnat-0.7.4
- ghc-typelits-extra-0.4.2
- ghc-typelits-natnormalise-0.7.3
- arrows-0.4.4.2
- Stream-0.4.7.2
- lazysmallcheck-0.6
- hedgehog-1.0.4
- tasty-hedgehog-1.0.1.0
flags:
clash-prelude:
multiple-hidden: false
So it's GHC 8.8.4 with the aforementioned Clash commit. I have only tested it by putting these definitions into a standalone Clash source file, not by patching clash-prelude
itself.
Works with GHC 8.10.3 as well.
I've pushed my full code (for GHC 8.10.3!) to https://github.com/gergoerdi/clash-issue-1629
The one thing I haven't tested is multiple-hidden: true
.
Right! Thanks, I'll test with multiple-hidden: False
!
That seems to work.
Sooooo I have never tried multiple-hidden: True
. Does it play nicely with the current Bundle
typeclass?
instance (Applicative f, Traversable f) => BundleX Bit f (f Bit) where instance (Applicative f, Traversable f) => BundleX (Maybe a) f (f (Maybe a)) where
You don't need constraints on f
for the do-nothing instances, since if you know f a ~ res
, you can always use id
without lifting that to f
.
As a small (perhaps superficial?) comment, changing the order of params to Bundle f a res
is nicer I think, for example:
instance Bundle f Bit (f Bit) where ...
instance Bundle f (a, b) (f a, f b) where ...
instance Bundle f (a, b, c) (f a, f b, f c) where ...
instance (KnownNat n) => Bundle f (Vec n a) (Vec n (f a)) where ...
Sooooo I have never tried
multiple-hidden: True
. Does it play nicely with the currentBundle
typeclass?
It does, but perhaps that's incidental on both being TF based solutions. Perhaps if we make both MTPC+FD solutions they'll also play nicely together. I do want to remark that multiple-hidden
is experimental and currently disabled for releases (even the upcoming 1.4 release), because there are still some issues with type-inference where you get horrible error messages. @martijnbastiaan knows best what is wrong with it exactly.
@gergoerdi I've created a draft PR over at https://github.com/clash-lang/clash-compiler/pull/1699, mostly to see how/when the test suite fails.
@martijnbastiaan knows best what is wrong with it exactly.
There are basically two things;
Poorer type inference. Multiple domains create more type ambiguity. Without it, a Hidden*
constraint always refers to exactly one implicit parameter, while it can refer to multiple with it. This is very similar to what polysemy-plugin solves and I think we could take a similar appraoch.
Poorer type errors. GHC already "pokes through" our HiddenClock dom
constraint synonyms from time to time, creating very confusing error messages for people not familiar with the underlying implementation (implicit parameters). This effect is put on steroids with multiple hidden clocks, as the underlying representation is even more confusing than the current one. I chatted with Richard Eisenberg a while back and he said work was underway to have GHC handle this more gracefully. I guess we should retest with 9.0!
And I guess there's a third point:
It seems that when I define Bundle
as:
class Bundle f a res | f a -> res, f res -> a, a res -> f
The multiple-hidden stuff does work.
Currently, there are two typeclasses (specific to
Signal
andDSignal
unbundling) that implement the same logic: turning, e.g.,f (a, b)
into(f a, f b)
. Couldn't these be unified into a single typeclass that doesn't care about the choice off
, as long as it is a traversable applicative functor?To illustrate, here's what it would look like:
And as a proof-of-concept, here are some instances: for an "atomic" type, for a tuple, and for
Vec
:Is there any hidden gotcha I am missing? If not, I would prefer moving over to this typeclass, to avoid having to manually dispatch between the
Signal
and theDSignal
one.