How to void a statement ?

[adfretlink]

I often have manipulation that return a value, that I will both use in a single manipulateParams call, or sometimes in batch with traversePrepared - in this latter case, I very frequently do not want the result and void it. This used to work fine in squeal 0.5, but it is my understanding that the new mechanisms at play in Squeal 0.6 make this a bit harder, as the compiler still tries to infer the voided type and fail unless I give it very explicitly.

It is however very convenient to be able to write:

void . traversePrepared -- .. statement and params

Sadly, I cannot use traversePrepared as it demands a statement that returns nothing - which makes sense.

So would it be possible to add a function voidStatement with a signature like this one:

-> Manipulation with db params ()

This way we could write:

traversePrepared . voidStatement -- .. statement and params

Unless there is a way of making traversePrepared_ work with manipulations that have a return type other than () ? (But it might not be a good idea either, as it is rather a good thing to have some type safety at this specific spot).

Obviously, this can still be worked around by stating the expected types explicitly, then voiding them, but it might be a nice convenience to add. What do you think ?

[echatav]

Three levels of statements

Low level: Query & Manipulation Mid level: Query_ & Manipulation_ (added in 0.5) High level: Statement (added in 0.6)

>>> :kind Query
Query :: FromType
         -> FromType -> SchemasType -> [NullType] -> RowType -> *
>>> :kind Query_
Query_ :: SchemasType -> * -> * -> *
>>> :kind Statement
Statement :: SchemasType -> * -> * -> *

Query_ is just a shorthand for Query because it has fewer variables and can calculate on Haskell types you may have around.

>>> :{
data Row col1 col2 col3 = Row
  {col1 :: col1, col2 :: col2, col3 :: col3}
  deriving stock GHC.Generic
  deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
:}
>>> :type undefined :: Query_ db (Int32,Char,Double) (Row String (Range Int16) (VarArray [Bool]))
undefined :: Query_ db (Int32,Char,Double) (Row String (Range Int16) (VarArray [Bool]))
  :: Query
       '[]
       '[]
       db
       '[ 'NotNull 'PGint4, 'NotNull ('PGchar 1), 'NotNull 'PGfloat8]
       '["col1" ::: 'NotNull 'PGtext,
         "col2" ::: 'NotNull ('PGrange 'PGint2),
         "col3" ::: 'NotNull ('PGvararray ('NotNull 'PGbool))]

So, functions that you have that work on Query should continue to work on Query_s.

But Query_s, I think, might be a bit of a misfeature. As a shorthand, it's ok. But it confuses things by sort of tricking the user into thinking they are typing things with Haskell types; when really, they're calculating a type family.

Statements fix this problem. Since they aren't a type family, they're (generalized algebraic) datatypes. But Statements aren't just the underlying Manipulation or Query, they also describe how to encode the Haskell input into SQL parameters and to DecodeRows into Haskell output. DecodeRow is a Functor and so, Statement is too.

What is the type of void?

>>> :type void
void :: Functor f => f a -> f ()
>>> :type void (undefined :: Statement db x y)
void (undefined :: Statement db x y) :: Statement db x ()

So, as you can see, you can directly void a Statement.

A Statement db x () can be executed over a Foldable container, with executePrepared_, so you can use executePrepared_ . void.

>>> :type executePrepared_ . void
executePrepared_ . void
  :: (MonadPQ db pq, Foldable list) =>
     Statement db x a -> list x -> pq ()

[adfretlink]

First off, let me apologize for my late answer, I don't have a lot of time available to work on upgrading my codebase to Squeal 0.6 so I had to delay answering till I could actually fiddle a bit.

Also, accept - again ! - all my thanks for a very clear and pedagogical answer, as always.

However, I'm afraid there are still some things where I'm not sure I follow you.

Indeed, in GHCI, your conclusion can be reproduced:

λ> :type executePrepared_ . void
executePrepared_ . void
  :: (MonadPQ db pq, Foldable list) =>
     Statement db x a -> list x -> pq ()

Similarly, I can absolutely do something like:

λ> :type void (undefined :: Statement db (Only Text) (Only Text))
void (undefined :: Statement db (Only Text) (Only Text))
  :: Statement db (Only Text) ()

However, things stop working once I'm trying to proceed from a Manipulation that I will turn into a statement. Obtaining a statement is not difficult, though the resulting type is a bit scary to look at:

λ> let manip = undefined :: Manipulation_ db (Only Text) (Only Text)
λ> :t manipulation manip
manipulation manip
  :: (FromField '("fromOnly", 'NotNull 'PGtext) t1, ToPG db t2,
      SOP.Generic x, SOP.Generic y,
      Generics.SOP.Record.ExtractTypesFromRecordCode '[t1]
      ~ Generics.SOP.Record.GetSingleton (SOP.Code y),
      SOP.Code x ~ '[ '[t2]], PG t2 ~ 'PGtext,
      Generics.SOP.Record.RecombineRecordCode
        (Generics.SOP.Record.ExtractLabelsFromRecordCode '[t1])
        (Generics.SOP.Record.GetSingleton (SOP.Code y))
      ~ '[t1],
      SOP.Code y ~ '[Generics.SOP.Record.GetSingleton (SOP.Code y)],
      Generics.SOP.Record.ToRecordCode_Datatype
        y (SOP.DatatypeInfoOf y) (SOP.Code y)
      ~ '[t1]) =>
     Statement db x y

I do have a typed manipulation manip, and I can morph it as a Statement through manipulation. But this resulting Statement cannot be voided:

λ> :t void (manipulation manip)

<interactive>:1:7: error:
    • Could not deduce: Generics.SOP.Record.ExtractTypesFromRecordCode
                          '[t0]
                        ~ Generics.SOP.Record.GetSingleton (SOP.Code a0)
        arising from a use of ‘manipulation’
      from the context: (ToPG db t, SOP.Generic x, SOP.Code x ~ '[ '[t]],
                         PG t ~ 'PGtext)
        bound by the inferred type of
                   it :: (ToPG db t, SOP.Generic x, SOP.Code x ~ '[ '[t]],
                          PG t ~ 'PGtext) =>
                         Statement db x ()
        at <interactive>:1:1
      The type variables ‘t0’, ‘a0’ are ambiguous
    • In the first argument of ‘void’, namely ‘(manipulation manip)’
      In the expression: void (manipulation manip)

From what I understand of GHC error, I cannot void statement if they have attached constraints, lest the compiler cannot follow what types the constraints are talking about.

Similary, your executePrepared_ . void cannot receive as parameter an actual Manipulation passed through manipulation. So I'm not sure I see how you can actually use that functorial property you underlined in your answer in practice.

I apologize in advance if I misunderstood your answer - I do feel like there's something I failed to grasp somewhere here, but I don't know exactly what !

[echatav]

So, the issue is that GHC cannot infer the Haskell input and output types, which is why, when you ask for the :type, it spits out a mess. You have to specify the types like.

>>> let manip = undefined :: Manipulation_ db (Only Text) (Only Text)
>>> let stmnt1 = manipulation manip :: Statement db (Only Text) (Only Text)

But that looks redundant, right? Why can't GHC infer those Haskell types without you specifying them a second time? The reason is that Manipulation_ is a non-injective type family, so GHC calculates on those Haskell types and then promptly forgets what they were.

>>> :type manip
manip
  :: Manipulation
       '[] db '[ 'NotNull 'PGtext] '["fromOnly" ::: 'NotNull 'PGtext]

So, Statements are where the actual Haskell types are fixed. But since we're there, we can streamline the type of the Statement.

>>> import Data.Profunctor
>>> let stmnt2 = dimap Only fromOnly stmnt1 :: Statement db Text Text

Statements let you do pre- and post-processing on the input and output. Or you can use explicit encoding and decoding.

>>> let stmnt3 = Manipulation aParam #fromOnly manip :: Statement db Text Text

[echatav]

If you still want to just traversePrepared_ over a "voided" Manipulation_ you could define:

>>> :{
let
  traverseVoided
    :: ( MonadPQ db pq
       , GenericParams db params x xs
       , Foldable list
       , SOP.SListI row )
    => Manipulation '[] db params row -> list x -> pq ()
  traverseVoided = executePrepared_ . Manipulation genericParams (return ())
:}

[adfretlink]

Wow, I think I finally got a grasp on what non injective type families mean thanks to your explanation ! I'll admit I never quite understood it, and always felt a bit scared when GHC used that expression. Yet another proof that Squeal is a great library to understand some of the trickier concepts used in haskell.

Again, thank you for your answer which clarified everything. Once I'm done upgrading my codebase (this is going to take a while though !), I will push a PR updating the tutorial I wrote so that it follows Squeal 0.6, it's the least I can do in exchange of all your help and great work.

[echatav]

In math we say a function f is injective iff for all x and x' in its domain, if f(x) = f(x') then x = x'. That is distinct inputs get mapped to distinct outputs. A non-injective function therefore maps some distinct inputs to the same output. For some x /= x', f(x) = f(x'). A type family is really just a type level function. So a non-injective type family F is one with two types X and X' which are distinct (don't unify according to GHC), but have the same output F X ~ F X'.