Lifting signal functions into DSignal

[gergoerdi]

I find myself using this definition:

liftD
    :: (HiddenClockResetEnable dom)
    => (forall dom'. (HiddenClockResetEnable dom') => Signal dom' a -> Signal dom' b)
    -> DSignal dom d a -> DSignal dom d b
liftD f = unsafeFromSignal . f . toSignal

but is it a good idea? Should it be generalized to

liftD
    :: (HiddenClockResetEnable dom)
    => SNat k
    -> (forall dom'. (HiddenClockResetEnable dom') => Signal dom' a -> Signal dom' b)
    -> DSignal dom d a -> DSignal dom (d + k) b
liftD SNat f = unsafeFromSignal . f . toSignal

?

Also, it is very painful to use for non-unary functions; for example:

liftD2
    :: (HiddenClockResetEnable dom)
    => (forall dom'. (HiddenClockResetEnable dom') => Signal dom' a -> Signal dom' b -> Signal dom' c)
    -> DSignal dom d a -> DSignal dom d b -> DSignal dom d c
liftD2 f x y = liftD (uncurry f . unbundle) $ liftA2 (,) x y

so I'd hope there are better points of the design space.

[gergoerdi]

so I'd hope there are better points of the design space.

Or should I say... the DSign space?

[christiaanb]

Perhaps we should just export the constructor for DSignal by default. Then liftD2 would simply Data.Coerce.coerce.

[christiaanb]

So we could add:

liftD ::
  forall d1 d2 dom a b .
  (Signal dom a -> Signal dom b) ->
  (DSignal dom d1 a -> DSignal dom d2 b)
liftD = coerce

liftD2 ::
  forall d1 d2 d3 dom a b c .
  (Signal dom a -> Signal dom b -> Signal dom c) ->
  (DSignal dom d1 a -> DSignal dom d2 b -> DSignal dom d3 c)
liftD2 = coerce

liftD3 ::
  forall d1 d2 d3 d4 dom a b c d .
  (Signal dom a -> Signal dom b -> Signal dom c -> Signal dom d) ->
  (DSignal dom d1 a -> DSignal dom d2 b -> DSignal dom d3 c -> DSignal dom d4 d)
liftD3 = coerce

or a more restrictive version:

liftD ::
  forall d1 d2 dom a b .
  (d1 <= d2) =>
  (Signal dom a -> Signal dom b) ->
  (DSignal dom d1 a -> DSignal dom d2 b)
liftD = coerce

liftD2 ::
  forall d1 d2 d3 dom a b c .
  (d1 <= d3, d2 <= d3) =>
  (Signal dom a -> Signal dom b -> Signal dom c) ->
  (DSignal dom d1 a -> DSignal dom d2 b -> DSignal dom d3 c)
liftD2 = coerce

liftD3 ::
  forall d1 d2 d3 d4 dom a b c d .
  (d1 <= d4, d2 <= d4, d3 <= d4) =>
  (Signal dom a -> Signal dom b -> Signal dom c -> Signal dom d) ->
  (DSignal dom d1 a -> DSignal dom d2 b -> DSignal dom d3 c -> DSignal dom d4 d)
liftD3 = coerce

which you can then use e.g.

{-# LANGUAGE PartialTypeSignatures #-}

fpAdd :: Signal dom Float -> Signal dom Float -> Signal dom Float
fpAdd = ...

fpAddD :: forall n . _
fpAddD = liftD2 @n @n @(n+3) fpAdd 

where fpAddD will of course get the inferred type:

fpAddD :: DSignal dom n Float -> DSignal dom n Float -> DSignal dom (n+3) Float