Selda: confused about type signtures

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
19 messages Options
Reply | Threaded
Open this post in threaded view
|

Selda: confused about type signtures

Marc Busqué
Hi!

I'm using [selda](https://hackage.haskell.org/package/selda) package in
order to deal with database backends.

Selda uses `TypeOperators` language extension, and it introduces  `:*:`
type operator constructor which take concrete types like `RowID` or
`Text` . It also has a `Table` type constructor which takes anything
built with `:*:`). On the other hand, `SeldaM` is selda custom monad
transformer with `IO` at the bottom.

I have following helper function which just wraps a call to the SQLite
backend. `dBPath` is just the database file path:

```
withDB :: SeldaM a -> IO a
withDB act = do
   path <- dBPath
   withSQLite path act
```

I want to wrap selda API in custom functions to be more resilient to
changes. Right now I'm trying to abstract selecting all rows for a given
table (maybe it seems brittle, but it is just a toy project in order to
learn Haskell):

```
list table = withDB $ query (select table)
```

Not adding a type signature to `list` produces following compilation
error:

```
• Non type-variable argument
     in the constraint: selda-0.1.12.1:Database.Selda.Column.Columns
                          (selda-0.1.12.1:Database.Selda.Column.Cols s a)
   (Use FlexibleContexts to permit this)
• When checking the inferred type
     list :: forall s a.
             (selda-0.1.12.1:Database.Selda.Column.Columns
                (selda-0.1.12.1:Database.Selda.Column.Cols s a),
              selda-0.1.12.1:Database.Selda.Compile.Result
                (selda-0.1.12.1:Database.Selda.Column.Cols s a)) =>
             Table a
             -> IO
                  [selda-0.1.12.1:Database.Selda.Compile.Res
                     (selda-0.1.12.1:Database.Selda.Column.Cols s a)]
```

If I try to add what I think would be the correct signature:

```
list :: Table a -> IO [a]
```

The error changes to:

```
• Couldn't match type ‘a’
                  with ‘selda-0.1.12.1:Database.Selda.Compile.Res
                          (selda-0.1.12.1:Database.Selda.Column.Cols s0 a)’
   ‘a’ is a rigid type variable bound by
     the type signature for:
       list :: forall a. Table a -> IO [a]
     at src/Hedger/Category.hs:35:1-25
   Expected type: SeldaM [a]
     Actual type: selda-0.1.12.1:Database.Selda.Backend.Internal.SeldaT
                    IO
                    [selda-0.1.12.1:Database.Selda.Compile.Res
                       (selda-0.1.12.1:Database.Selda.Column.Cols s0 a)]
• In the second argument of ‘($)’, namely ‘query (select table)’
   In the expression: withDB $ query (select table)
   In an equation for ‘list’:
       list table = withDB $ query (select table)
• Relevant bindings include
     table :: Table a (bound at src/Hedger/Category.hs:36:6)
     list :: Table a -> IO [a] (bound at src/Hedger/Category.hs:36:1)
    |
36 | list table = withDB $ query (select table)
```

However, if I constraint the type signature to act just for a given
table, it compiles without errors:

```
type CategoriesSchema = RowID:*:Text
list :: Table CategoriesSchema -> IO [CategoriesSchema]
```

Why is that it works with concrete types but not with a type variable
that takes the same concrete type in its both placeholders?

Thanks in advance,

Marc Busqué
http://waiting-for-dev.github.io/about/
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Selda: confused about type signtures

Tom Ellis
On Fri, Apr 20, 2018 at 08:33:10PM +0200, Marc Busqué wrote:
> Not adding a type signature to `list` produces following compilation
> error:
>
[...]
>   (Use FlexibleContexts to permit this)
>
> Why is that it works with concrete types but not with a type variable
> that takes the same concrete type in its both placeholders?

Did you try applying the suggested fix?  Explicitly, add

{-# LANGUAGE FlexibleContexts #-}

at the top of your file to permit this.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Selda: confused about type signtures

Marc Busqué
On Fri, 20 Apr 2018, Tom Ellis wrote:

> Did you try applying the suggested fix?  Explicitly, add
>
> {-# LANGUAGE FlexibleContexts #-}
>
> at the top of your file to permit this.

It doesn't work neither. In this case the error is:

```
• Couldn't match type ‘selda-0.1.12.1:Database.Selda.Compile.Res
                          (selda-0.1.12.1:Database.Selda.Column.Cols s0 a)’
                  with ‘selda-0.1.12.1:Database.Selda.Compile.Res
                          (selda-0.1.12.1:Database.Selda.Column.Cols s a)’
   Expected type: Table a
                  -> IO
                       [selda-0.1.12.1:Database.Selda.Compile.Res
                          (selda-0.1.12.1:Database.Selda.Column.Cols s a)]
     Actual type: Table a
                  -> IO
                       [selda-0.1.12.1:Database.Selda.Compile.Res
                          (selda-0.1.12.1:Database.Selda.Column.Cols s0 a)]
   NB: ‘selda-0.1.12.1:Database.Selda.Compile.Res’ is a type function, and may not be injective
   The type variable ‘s0’ is ambiguous
• In the ambiguity check for the inferred type for ‘list’
   To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
   When checking the inferred type
     list :: forall s a.
             (selda-0.1.12.1:Database.Selda.Column.Columns
                (selda-0.1.12.1:Database.Selda.Column.Cols s a),
              selda-0.1.12.1:Database.Selda.Compile.Result
                (selda-0.1.12.1:Database.Selda.Column.Cols s a)) =>
             Table a
             -> IO
                  [selda-0.1.12.1:Database.Selda.Compile.Res
                     (selda-0.1.12.1:Database.Selda.Column.Cols s a)]
    |
36 | list table = withDB $ query (select table)
```

Anyway, I'm more interested in understanding an explicit type signature,
in this case.

Marc Busqué
http://waiting-for-dev.github.io/about/
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Selda: confused about type signtures

Brandon Allbery
In reply to this post by Marc Busqué
The more precise answer to your question is that an explicit type signature is taken as exact. If the type needed is some (Ctx a => a), as here, but your type signature just says a, you will get a type error exactly as you did.

"a" there does not mean "figure out a type for me". It means *any type at all*. Including Void, (), Int, etc., which one would not expect to work there.

On Fri, Apr 20, 2018 at 2:33 PM, Marc Busqué <[hidden email]> wrote:
Hi!

I'm using [selda](https://hackage.haskell.org/package/selda) package in
order to deal with database backends.

Selda uses `TypeOperators` language extension, and it introduces  `:*:`
type operator constructor which take concrete types like `RowID` or
`Text` . It also has a `Table` type constructor which takes anything
built with `:*:`). On the other hand, `SeldaM` is selda custom monad
transformer with `IO` at the bottom.

I have following helper function which just wraps a call to the SQLite
backend. `dBPath` is just the database file path:

```
withDB :: SeldaM a -> IO a
withDB act = do
  path <- dBPath
  withSQLite path act
```

I want to wrap selda API in custom functions to be more resilient to
changes. Right now I'm trying to abstract selecting all rows for a given
table (maybe it seems brittle, but it is just a toy project in order to
learn Haskell):

```
list table = withDB $ query (select table) ```

Not adding a type signature to `list` produces following compilation
error:

```
• Non type-variable argument
    in the constraint: selda-0.1.12.1:Database.Selda.Column.Columns
                         (selda-0.1.12.1:Database.Selda.Column.Cols s a)
  (Use FlexibleContexts to permit this)
• When checking the inferred type
    list :: forall s a.
            (selda-0.1.12.1:Database.Selda.Column.Columns
               (selda-0.1.12.1:Database.Selda.Column.Cols s a),
             selda-0.1.12.1:Database.Selda.Compile.Result
               (selda-0.1.12.1:Database.Selda.Column.Cols s a)) =>
            Table a
            -> IO
                 [selda-0.1.12.1:Database.Selda.Compile.Res
                    (selda-0.1.12.1:Database.Selda.Column.Cols s a)]
```

If I try to add what I think would be the correct signature:

```
list :: Table a -> IO [a]
```

The error changes to:

```
• Couldn't match type ‘a’
                 with ‘selda-0.1.12.1:Database.Selda.Compile.Res
                         (selda-0.1.12.1:Database.Selda.Column.Cols s0 a)’
  ‘a’ is a rigid type variable bound by
    the type signature for:
      list :: forall a. Table a -> IO [a]
    at src/Hedger/Category.hs:35:1-25
  Expected type: SeldaM [a]
    Actual type: selda-0.1.12.1:Database.Selda.Backend.Internal.SeldaT
                   IO
                   [selda-0.1.12.1:Database.Selda.Compile.Res
                      (selda-0.1.12.1:Database.Selda.Column.Cols s0 a)]
• In the second argument of ‘($)’, namely ‘query (select table)’
  In the expression: withDB $ query (select table)
  In an equation for ‘list’:
      list table = withDB $ query (select table)
• Relevant bindings include
    table :: Table a (bound at src/Hedger/Category.hs:36:6)
    list :: Table a -> IO [a] (bound at src/Hedger/Category.hs:36:1)
   |
36 | list table = withDB $ query (select table)
```

However, if I constraint the type signature to act just for a given
table, it compiles without errors:

```
type CategoriesSchema = RowID:*:Text
list :: Table CategoriesSchema -> IO [CategoriesSchema]
```

Why is that it works with concrete types but not with a type variable
that takes the same concrete type in its both placeholders?

Thanks in advance,

Marc Busqué
http://waiting-for-dev.github.io/about/
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.



--
brandon s allbery kf8nh                               sine nomine associates
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Selda: confused about type signtures

Marc Busqué
On Fri, 20 Apr 2018, Brandon Allbery wrote:

> The more precise answer to your question is that an explicit type signature is taken as exact. If the type needed is some (Ctx a => a), as here,
> but your type signature just says a, you will get a type error exactly as you did.
> "a" there does not mean "figure out a type for me". It means *any type at all*. Including Void, (), Int, etc., which one would not expect to work
> there.

Thanks! That was an illuminating answer :)

Marc Busqué
http://waiting-for-dev.github.io/about/
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Selda: confused about type signtures

Marc Busqué
In reply to this post by Brandon Allbery
On Fri, 20 Apr 2018, Brandon Allbery wrote:

> The more precise answer to your question is that an explicit type signature is taken as exact. If the type needed is some (Ctx a => a), as here,
> but your type signature just says a, you will get a type error exactly as you did.
> "a" there does not mean "figure out a type for me". It means *any type at all*. Including Void, (), Int, etc., which one would not expect to work
> there.

I'm still in troubles with this...

If I add `FlexibleContexts` and `AllowAmbiguosTypes` extensions, I can
compile the program and ask for the type of `list`:

```
:t list
--- list
---   :: (selda-0.1.12.1:Database.Selda.Compile.Result
---         (selda-0.1.12.1:Database.Selda.Column.Cols s a),
---       selda-0.1.12.1:Database.Selda.Column.Columns
---         (selda-0.1.12.1:Database.Selda.Column.Cols s a)) =>
---      selda-0.1.12.1:Database.Selda.Table.Table a
---      -> IO
---           [selda-0.1.12.1:Database.Selda.Compile.Res
---              (selda-0.1.12.1:Database.Selda.Column.Cols s a)]
```

However, manually adding this same type:

```
list :: (Result (Cols s a), Columns (Cols s a))  => Table a -> IO [Res (Cols s a)]
list table = withDB $ query (select table)
```

results in a compilation error:

```
• Couldn't match type ‘Res (Cols s0 a)’ with ‘Res (Cols s a)’
   Expected type: IO [Res (Cols s a)]
     Actual type: IO [Res (Cols s0 a)]
   NB: ‘Res’ is a type function, and may not be injective
   The type variable ‘s0’ is ambiguous
• In the expression: withDB $ query (select table)
   In an equation for ‘list’:
       list table = withDB $ query (select table)
• Relevant bindings include
     table :: Table a (bound at src/Hedger/Category.hs:44:6)
     list :: Table a -> IO [Res (Cols s a)]
       (bound at src/Hedger/Category.hs:44:1)
    |
44 | list table = withDB $ query (select table)
```

I'm pretty sure that my error is related with what is exposed in this
page in the wiki: https://wiki.haskell.org/GHC/TypeSigsAndAmbiguity

But I'm not sure about how I could fix that. At the end of the article
it is said that this only happen in programs that "they could never
really work". But, if I'm not missing something, that function does work.
I have tried it with the auto-inferred signature way and it indeed can
list rows for different database tables.

I leave here more info just in case it is useful:

```
:t select
--- select :: Columns (Cols s a) => Table a -> Query s (Cols s a)

:t query
--- query :: (Result a, MonadSelda m) => Query s a -> m [Res a]

:t withDB
--- withDB :: SeldaM a -> IO a

:info Columns
class Columns a where
--- selda-0.1.12.1:Database.Selda.Column.toTup :: [ColName] -> a
--- selda-0.1.12.1:Database.Selda.Column.fromTup :: a
---                                                   -> [selda-0.1.12.1:Database.Selda.Exp.SomeCol
---                                                         selda-0.1.12.1:Database.Selda.SQL.SQL]
---   {-# MINIMAL toTup, fromTup #-}
---   -- Defined in ‘selda-0.1.12.1:Database.Selda.Column’
--- instance forall k (s :: k) a. Columns (Col s a)
---   -- Defined in ‘selda-0.1.12.1:Database.Selda.Column’
--- instance forall k b (s :: k) a.
---          Columns b =>
---          Columns (Col s a :*: b)
---   -- Defined in ‘selda-0.1.12.1:Database.Selda.Column’

:info Cols
--- type family Cols (s :: k) a :: *
---   where
---     [k, (s :: k), a, b] Cols k s (a :*: b) = Col s a :*: Cols s b
---     [k, (s :: k), a] Cols k s a = Col s a
---   -- Defined in ‘selda-0.1.12.1:Database.Selda.Column’

:info Result
--- class base-4.10.1.0:Data.Typeable.Internal.Typeable (Res r) =>
---       Result r where
---   type family Res r :: *
---   selda-0.1.12.1:Database.Selda.Compile.toRes :: Data.Proxy.Proxy r
---                                                  -> [selda-0.1.12.1:Database.Selda.SqlType.SqlValue]
---                                                  -> Res r
---   selda-0.1.12.1:Database.Selda.Compile.finalCols :: r
---                                                      -> [selda-0.1.12.1:Database.Selda.Exp.SomeCol
---                                                            selda-0.1.12.1:Database.Selda.SQL.SQL]
---   {-# MINIMAL toRes, finalCols #-}
---   -- Defined in ‘selda-0.1.12.1:Database.Selda.Compile’
--- instance SqlType a => Result (Col s a)
---   -- Defined in ‘selda-0.1.12.1:Database.Selda.Compile’
--- instance (SqlType a, Result b) => Result (Col s a :*: b)
---   -- Defined in ‘selda-0.1.12.1:Database.Selda.Compile’

:info Res
--- class base-4.10.1.0:Data.Typeable.Internal.Typeable (Res r) =>
---       Result r where
---   type family Res r :: *
---   ...
---   -- Defined in ‘selda-0.1.12.1:Database.Selda.Compile’
--- type instance Res (Col s a) = a
---   -- Defined in ‘selda-0.1.12.1:Database.Selda.Compile’
--- type instance Res (Col s a :*: b) = a :*: Res b
---   -- Defined in ‘selda-0.1.12.1:Database.Selda.Compile’

:info Table
--- type role Table phantom
--- data Table a
---   = selda-0.1.12.1:Database.Selda.Table.Table {selda-0.1.12.1:Database.Selda.Table.tableName :: TableName,
---                                                selda-0.1.12.1:Database.Selda.Table.tableCols :: [selda-0.1.12.1:Database.Selda.Table.ColInfo],
---                                                selda-0.1.12.1:Database.Selda.Table.tableHasAutoPK :: Bool}
---   -- Defined in ‘selda-0.1.12.1:Database.Selda.Table’
```

Marc Busqué
http://waiting-for-dev.github.io/about/

>
> On Fri, Apr 20, 2018 at 2:33 PM, Marc Busqué <[hidden email]> wrote:
>       Hi!
>
>       I'm using [selda](https://hackage.haskell.org/package/selda) package in
>       order to deal with database backends.
>
>       Selda uses `TypeOperators` language extension, and it introduces  `:*:`
>       type operator constructor which take concrete types like `RowID` or
>       `Text` . It also has a `Table` type constructor which takes anything
>       built with `:*:`). On the other hand, `SeldaM` is selda custom monad
>       transformer with `IO` at the bottom.
>
>       I have following helper function which just wraps a call to the SQLite
>       backend. `dBPath` is just the database file path:
>
>       ```
>       withDB :: SeldaM a -> IO a
>       withDB act = do
>         path <- dBPath
>         withSQLite path act
>       ```
>
>       I want to wrap selda API in custom functions to be more resilient to
>       changes. Right now I'm trying to abstract selecting all rows for a given
>       table (maybe it seems brittle, but it is just a toy project in order to
>       learn Haskell):
>
>       ```
>       list table = withDB $ query (select table) ```
>
>       Not adding a type signature to `list` produces following compilation
>       error:
>
>       ```
>       • Non type-variable argument
>           in the constraint: selda-0.1.12.1:Database.Selda.Column.Columns
>                                (selda-0.1.12.1:Database.Selda.Column.Cols s a)
>         (Use FlexibleContexts to permit this)
>       • When checking the inferred type
>           list :: forall s a.
>                   (selda-0.1.12.1:Database.Selda.Column.Columns
>                      (selda-0.1.12.1:Database.Selda.Column.Cols s a),
>                    selda-0.1.12.1:Database.Selda.Compile.Result
>                      (selda-0.1.12.1:Database.Selda.Column.Cols s a)) =>
>                   Table a
>                   -> IO
>                        [selda-0.1.12.1:Database.Selda.Compile.Res
>                           (selda-0.1.12.1:Database.Selda.Column.Cols s a)]
>       ```
>
>       If I try to add what I think would be the correct signature:
>
>       ```
>       list :: Table a -> IO [a]
>       ```
>
>       The error changes to:
>
>       ```
>       • Couldn't match type ‘a’
>                        with ‘selda-0.1.12.1:Database.Selda.Compile.Res
>                                (selda-0.1.12.1:Database.Selda.Column.Cols s0 a)’
>         ‘a’ is a rigid type variable bound by
>           the type signature for:
>             list :: forall a. Table a -> IO [a]
>           at src/Hedger/Category.hs:35:1-25
>         Expected type: SeldaM [a]
>           Actual type: selda-0.1.12.1:Database.Selda.Backend.Internal.SeldaT
>                          IO
>                          [selda-0.1.12.1:Database.Selda.Compile.Res
>                             (selda-0.1.12.1:Database.Selda.Column.Cols s0 a)]
>       • In the second argument of ‘($)’, namely ‘query (select table)’
>         In the expression: withDB $ query (select table)
>         In an equation for ‘list’:
>             list table = withDB $ query (select table)
>       • Relevant bindings include
>           table :: Table a (bound at src/Hedger/Category.hs:36:6)
>           list :: Table a -> IO [a] (bound at src/Hedger/Category.hs:36:1)
>          |
>       36 | list table = withDB $ query (select table)
>       ```
>
>       However, if I constraint the type signature to act just for a given
>       table, it compiles without errors:
>
>       ```
>       type CategoriesSchema = RowID:*:Text
>       list :: Table CategoriesSchema -> IO [CategoriesSchema]
>       ```
>
>       Why is that it works with concrete types but not with a type variable
>       that takes the same concrete type in its both placeholders?
>
>       Thanks in advance,
>
>       Marc Busqué
>       http://waiting-for-dev.github.io/about/
>       _______________________________________________
>       Haskell-Cafe mailing list
>       To (un)subscribe, modify options or view archives go to:
>       http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>       Only members subscribed via the mailman list are allowed to post.
>
>
>
>
> --
> brandon s allbery kf8nh                               sine nomine associates
> [hidden email]                                  [hidden email]
> unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net
>
>
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Selda: confused about type signtures

Tom Ellis
On Sun, Apr 22, 2018 at 08:21:11PM +0200, Marc Busqué wrote:

> If I add `FlexibleContexts` and `AllowAmbiguosTypes` extensions, I can
> compile the program and ask for the type of `list`:
>
> ```
> :t list --- list
> ---   :: (selda-0.1.12.1:Database.Selda.Compile.Result
> ---         (selda-0.1.12.1:Database.Selda.Column.Cols s a),
> ---       selda-0.1.12.1:Database.Selda.Column.Columns
> ---         (selda-0.1.12.1:Database.Selda.Column.Cols s a)) =>
> ---      selda-0.1.12.1:Database.Selda.Table.Table a
> ---      -> IO
> ---           [selda-0.1.12.1:Database.Selda.Compile.Res
> ---              (selda-0.1.12.1:Database.Selda.Column.Cols s a)]
> ```
>
> However, manually adding this same type:
>
> ```
> list :: (Result (Cols s a), Columns (Cols s a))  => Table a -> IO [Res (Cols s a)]
> list table = withDB $ query (select table)
> ```
>
> results in a compilation error:

Unless I am much mistaken `Cols s a` is just `a`[1,2].  That explains why
the type is ambiguous.  There's nothing that fixes `s`.

> But I'm not sure about how I could fix that. At the end of the article
> it is said that this only happen in programs that "they could never
> really work". But, if I'm not missing something, that function does work.
> I have tried it with the auto-inferred signature way and it indeed can
> list rows for different database tables.

Can you show us a minimal example of `list` working?  I'm quite confused
about how it could work.

Tom


[1] https://www.stackage.org/haddock/lts-9.14/selda-0.1.11.1/src/Database.Selda.Compile.html#line-126)

[2] https://www.stackage.org/haddock/lts-9.14/selda-0.1.11.1/Database-Selda.html#t:Cols
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Selda: confused about type signtures

Marc Busqué
On Sun, 22 Apr 2018, Tom Ellis wrote:

> Unless I am much mistaken `Cols s a` is just `a`[1,2].  That explains why
> the type is ambiguous.  There's nothing that fixes `s`.

I also thought that, but if I substitute `Cols s a` by `a`, then the
compilation error is:

```
• Couldn't match type ‘Res (Cols s0 a)’ with ‘Res a’
   Expected type: IO [Res a]
     Actual type: IO [Res (Cols s0 a)]
   NB: ‘Res’ is a type function, and may not be injective
   The type variable ‘s0’ is ambiguous
• In the expression: withDB $ query (select table)
   In an equation for ‘list’:
       list table = withDB $ query (select table)
• Relevant bindings include
     table :: Table a (bound at src/Hedger/Category.hs:44:6)
     list :: Table a -> IO [Res a]
       (bound at src/Hedger/Category.hs:44:1)
    |
44 | list table = withDB $ query (select table)
```

Also, notice that the inferred type does differentiate between `Cols s a` and `a`.

> Can you show us a minimal example of `list` working?  I'm quite confused
> about how it could work.

```
type CategoriesSchema = RowID:*:Text
type ExpensesSchema = RowID:*:Text:*:Double:*:RowID

categories:: Table (CategoriesSchema)
(categories, categoryID :*: rest) = tableWithSelectors "categories"
     $ autoPrimary "id"
     :*: required "name"

expenses:: Table (ExpensesSchema)
expenses = table "expenses"
     $ autoPrimary "id"
     :*: required "name"
     :*: required "amount"
     :*: required "category_id" `fk` (categories, categoryID)

withDB (tryCreateTable categories)
withDB (tryCreateTable expenses)

withDB $ insert_ categories [ def :*: "foo" ]

list categories
--- [1 :*: "foo"]

list expenses
--- []

Marc Busqué
http://waiting-for-dev.github.io/about/
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Selda: confused about type signtures

Li-yao Xia-2
In reply to this post by Marc Busqué
Hi Marc,

> ```
> list :: (Result (Cols s a), Columns (Cols s a))  => Table a -> IO [Res
> (Cols s a)]
> list table = withDB $ query (select table)
> ```

The only occurence of `s`/`s0` that is not ambiguous is between `select`
and `query`, as the first argument of the data type `Query`. Everywhere
else, there is a type family in the way which prevents unification; for
example `Cols s a ~ Cols s0 a` does not imply `s ~ s0`.

You can use a type annotation or TypeApplications to instantiate the
`s0` between `query` and `select`. This requires ScopedTypeVariables,
and an explicit `forall` at the top to make the type variables available
in the definition body.

Note that the type of `list` is also ambiguous for the aforementioned
reasons, since `s` is only an argument of the type family `Res` (and
`Cols`). You will have to AllowAmbiguousTypes to define it and write
`list @s` (with TypeApplications) to use it.

```
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

list :: forall s a. (Result (Cols s a), Columns (Cols s a))
      => Table a -> IO [Res (Cols s a)]
list table = withDB $ query (select table :: Query s _)
-- or,                  ... (select @s table)
-- with {-# LANGUAGE TypeApplications #-}
```

References in the GHC manual:

- ScopedTypeVariables:
https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#lexically-scoped-type-variables

- TypeApplications:
https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#visible-type-application

- AllowAmbiguousTypes:
https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#ambiguous-types-and-the-ambiguity-check

Li-yao
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Selda: confused about type signtures

Tom Ellis
In reply to this post by Marc Busqué
On Mon, Apr 23, 2018 at 09:23:58AM +0200, Marc Busqué wrote:
> On Sun, 22 Apr 2018, Tom Ellis wrote:
> >Unless I am much mistaken `Cols s a` is just `a`[1,2].  That explains why
> >the type is ambiguous.  There's nothing that fixes `s`.
>
> I also thought that, but if I substitute `Cols s a` by `a`, then the
> compilation error is:

I had an error in what I said and also it was imprecise.  It's
`Res (Cols s a)` which is `a`, but only in the cases where you're actually
going to use it, and the compiler cannot take that into account when
solving the constraint.  Anyway, as Li-yao Xia points out in a sibling
message, the type variable `s` in not constrained and therefore it seems
impossible to solve.

> Also, notice that the inferred type does differentiate between `Cols s a` and `a`.
>
> >Can you show us a minimal example of `list` working?  I'm quite confused
> >about how it could work.
[...]

Thanks, but could you send a full working version that includes a definition
of `list`?  I can't replicate what you've done on my end.

Tom

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Selda: confused about type signtures

Tom Ellis
On Mon, Apr 23, 2018 at 01:16:50PM +0100, Tom Ellis wrote:
> Thanks, but could you send a full working version that includes a definition
> of `list`?  I can't replicate what you've done on my end.

And what GHC version are you using?  I can't replicate this on 7.10 or 8.0.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Selda: confused about type signtures

Marc Busqué
In reply to this post by Li-yao Xia-2
On Mon, 23 Apr 2018, Li-yao Xia wrote:

> Hi Marc,
>
>> ```
>> list :: (Result (Cols s a), Columns (Cols s a))  => Table a -> IO [Res
>> (Cols s a)]
>> list table = withDB $ query (select table)
>> ```
>
> The only occurence of `s`/`s0` that is not ambiguous is between `select` and
> `query`, as the first argument of the data type `Query`. Everywhere else,
> there is a type family in the way which prevents unification; for example
> `Cols s a ~ Cols s0 a` does not imply `s ~ s0`.
>
> You can use a type annotation or TypeApplications to instantiate the `s0`
> between `query` and `select`. This requires ScopedTypeVariables, and an
> explicit `forall` at the top to make the type variables available in the
> definition body.
>
> Note that the type of `list` is also ambiguous for the aforementioned
> reasons, since `s` is only an argument of the type family `Res` (and `Cols`).
> You will have to AllowAmbiguousTypes to define it and write `list @s` (with
> TypeApplications) to use it.
>
> ```
> {-# LANGUAGE AllowAmbiguousTypes #-}
> {-# LANGUAGE ScopedTypeVariables #-}
>
> list :: forall s a. (Result (Cols s a), Columns (Cols s a))
>     => Table a -> IO [Res (Cols s a)]
> list table = withDB $ query (select table :: Query s _)
> -- or,                  ... (select @s table)
> -- with {-# LANGUAGE TypeApplications #-}
> ```
>
> References in the GHC manual:
>
> - ScopedTypeVariables:
> https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#lexically-scoped-type-variables
>
> - TypeApplications:
> https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#visible-type-application
>
> - AllowAmbiguousTypes:
> https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#ambiguous-types-and-the-ambiguity-check
>
> Li-yao
Thanks Li-yao. I'll studiy it thoroughly. It looks promising.

Marc Busqué
http://waiting-for-dev.github.io/about/
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Selda: confused about type signtures

Marc Busqué
In reply to this post by Tom Ellis
On Mon, 23 Apr 2018, Tom Ellis wrote:

> I had an error in what I said and also it was imprecise.  It's
> `Res (Cols s a)` which is `a`, but only in the cases where you're actually
> going to use it, and the compiler cannot take that into account when
> solving the constraint.  Anyway, as Li-yao Xia points out in a sibling
> message, the type variable `s` in not constrained and therefore it seems
> impossible to solve.

Thanks Tom for your reply.

In this case the error is:

```
• Couldn't match type ‘a’ with ‘Res (Cols s0 a)’
       ‘a’ is a rigid type variable bound by
         the type signature for:
           list :: forall s a.
                   (Result (Cols s a), Columns (Cols s a)) =>
                   Table a -> IO [a]
         at src/Hedger/Backend.hs:24:1-69
       Expected type: selda-0.1.12.1:Database.Selda.Backend.Internal.SeldaM
                        [a]
         Actual type: selda-0.1.12.1:Database.Selda.Backend.Internal.SeldaT
                        IO [Res (Cols s0 a)]
     • In the second argument of ‘($)’, namely ‘query (select table)’
       In the expression: withDB $ query (select table)
       In an equation for ‘list’:
           list table = withDB $ query (select table)
     • Relevant bindings include
         table :: Table a (bound at src/Hedger/Backend.hs:25:6)
         list :: Table a -> IO [a] (bound at src/Hedger/Backend.hs:25:1)
    |
25 | list table = withDB $ query (select table)
```
> Thanks, but could you send a full working version that includes a definition
> of `list`?  I can't replicate what you've done on my end.

I have pushed the repo to Github:

https://github.com/waiting-for-dev/hedger

Important code is in `src/Hedger/` directory.

`Backend.hs` is where `list` is defined. Right now it has its type
signature commented out so that it compiles thanks to
`AllowAmbiguosTypes` and `FlexibleContexts`.

`Category.hs` has the function `listCategories` which uses `list`.
Anyway, from `ghci` one can just call `list categories` or `list
expenses`. There is also a helper function `addCategory` to add a
category record just providing its name (from `ghci`,
`OverloadedStrings` must be loaded).

In `Migration.hs` is where `categories` and `expenses` tables are
created.

Marc Busqué
http://waiting-for-dev.github.io/about/
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Selda: confused about type signtures

Marc Busqué
In reply to this post by Tom Ellis
On Mon, 23 Apr 2018, Tom Ellis wrote:

> And what GHC version are you using?  I can't replicate this on 7.10 or 8.0.

I'm on 8.2.2.

Marc Busqué
http://waiting-for-dev.github.io/about/
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Selda: confused about type signtures

Tom Ellis
In reply to this post by Marc Busqué
On Mon, Apr 23, 2018 at 04:54:36PM +0200, Marc Busqué wrote:

> On Mon, 23 Apr 2018, Tom Ellis wrote:
> >I had an error in what I said and also it was imprecise.  It's
> >`Res (Cols s a)` which is `a`, but only in the cases where you're actually
> >going to use it, and the compiler cannot take that into account when
> >solving the constraint.  Anyway, as Li-yao Xia points out in a sibling
> >message, the type variable `s` in not constrained and therefore it seems
> >impossible to solve.
>
> I have pushed the repo to Github:
>
> https://github.com/waiting-for-dev/hedger

Thanks for that Marc, it's very helpful.  I extracted the parts that are
relevant to the problem and created a version that doesn't depend on Selda:

    https://gist.github.com/tomjaguarpaw/f4db46671e2f39b790a25b8907dc53a3

I think I now understand what the situation is.  Interestingly your code
works on 8.0 but not 7.10.

Contrary to my earlier presumptions, the compiler *is* able to give a type
to `list` because `Cols` is a closed type family.  I suppose it can
determine that `Cols s a` does not actually depend on `s` so giving list the
type

    (Result (Cols s a), Columns (Cols s a)) => Table a -> Res (Cols s a)

is fine.  The type of `s` will never be needed.  When `list` is applied to
`categories` then `a` is fixed and `Res (Cols s a)` is fixed, regardless of
what `s` is.

Subtly changing the definition of Cols will break things.  For example, if
you add the clause

        Cols () a = Col Int a

then you won't be able to define `list` any more, even though `Res (Cols s
a)` is still just `a` because the `Columns (Cols s a)` instance might then
depend on what `s` is.

On the other hand, I do not yet understand why you cannot provide an
explicit signature for `list`.  I suspect this is some hairy compiler bug.
Either it should be possible to give `list` its inferred type or it should
be forbidden.  It's probably worth filing an issue about this on GHC Trac.
I would be interested to hear Li-yao's thoughts on the matter.

Incidentally, this is why I try to avoid type families as much as possible.
When they go wrong it's very hard to understand why, and indeed when they go
right it's also very hard to understand why.

Tom
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Selda: confused about type signtures

Marc Busqué
Tom, thank you very much for your deep inspection. Your gist can be
really helpful in trying to understand the problem. I will study it
carefully. I have been reading books about Haskell and also Category
Theory for some months, but I have just started coding few weeks ago, so
I'm bit overwhelmed about having found a compiler bug so soon :D I'll
look into all of this and also about Li-yao recommendations and if it is
suitable I'll fill the issue and also report here.

Marc Busqué
http://waiting-for-dev.github.io/about/

On Mon, 23 Apr 2018, Tom Ellis wrote:

> On Mon, Apr 23, 2018 at 04:54:36PM +0200, Marc Busqué wrote:
>> On Mon, 23 Apr 2018, Tom Ellis wrote:
>> >I had an error in what I said and also it was imprecise.  It's
>> >`Res (Cols s a)` which is `a`, but only in the cases where you're actually
>> >going to use it, and the compiler cannot take that into account when
>> >solving the constraint.  Anyway, as Li-yao Xia points out in a sibling
>> >message, the type variable `s` in not constrained and therefore it seems
>> >impossible to solve.
>>
>> I have pushed the repo to Github:
>>
>> https://github.com/waiting-for-dev/hedger
>
> Thanks for that Marc, it's very helpful.  I extracted the parts that are
> relevant to the problem and created a version that doesn't depend on Selda:
>
>    https://gist.github.com/tomjaguarpaw/f4db46671e2f39b790a25b8907dc53a3
>
> I think I now understand what the situation is.  Interestingly your code
> works on 8.0 but not 7.10.
>
> Contrary to my earlier presumptions, the compiler *is* able to give a type
> to `list` because `Cols` is a closed type family.  I suppose it can
> determine that `Cols s a` does not actually depend on `s` so giving list the
> type
>
>    (Result (Cols s a), Columns (Cols s a)) => Table a -> Res (Cols s a)
>
> is fine.  The type of `s` will never be needed.  When `list` is applied to
> `categories` then `a` is fixed and `Res (Cols s a)` is fixed, regardless of
> what `s` is.
>
> Subtly changing the definition of Cols will break things.  For example, if
> you add the clause
>
>        Cols () a = Col Int a
>
> then you won't be able to define `list` any more, even though `Res (Cols s
> a)` is still just `a` because the `Columns (Cols s a)` instance might then
> depend on what `s` is.
>
> On the other hand, I do not yet understand why you cannot provide an
> explicit signature for `list`.  I suspect this is some hairy compiler bug.
> Either it should be possible to give `list` its inferred type or it should
> be forbidden.  It's probably worth filing an issue about this on GHC Trac.
> I would be interested to hear Li-yao's thoughts on the matter.
>
> Incidentally, this is why I try to avoid type families as much as possible.
> When they go wrong it's very hard to understand why, and indeed when they go
> right it's also very hard to understand why.
>
> Tom
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Selda: confused about type signtures

Tom Ellis
Marc, you're doing very impressively if this is the beginning of your
Haskell career!  Do feel free to keep asking here if you have more
questions.

On Mon, Apr 23, 2018 at 08:08:18PM +0200, Marc Busqué wrote:
> Tom, thank you very much for your deep inspection. Your gist can be
> really helpful in trying to understand the problem. I will study it
> carefully. I have been reading books about Haskell and also Category
> Theory for some months, but I have just started coding few weeks ago, so
> I'm bit overwhelmed about having found a compiler bug so soon :D I'll
> look into all of this and also about Li-yao recommendations and if it is
> suitable I'll fill the issue and also report here.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Selda: confused about type signtures

Marc Busqué
On Mon, 23 Apr 2018, Tom Ellis wrote:

> Marc, you're doing very impressively if this is the beginning of your
> Haskell career!  Do feel free to keep asking here if you have more
> questions.

Thanks for your encouragement :)

Marc Busqué
http://waiting-for-dev.github.io/about/
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Selda: confused about type signtures

Marc Busqué
In reply to this post by Li-yao Xia-2
Just for completeness about this solution:

On Mon, 23 Apr 2018, Li-yao Xia wrote:

> ```
> {-# LANGUAGE AllowAmbiguousTypes #-}
> {-# LANGUAGE ScopedTypeVariables #-}
>
> list :: forall s a. (Result (Cols s a), Columns (Cols s a))
>     => Table a -> IO [Res (Cols s a)]
> list table = withDB $ query (select table :: Query s _)

This gives error:

```
     • Couldn't match type ‘Res a’ with ‘Res (Cols s a)’
       Expected type: IO [Res (Cols s a)]
         Actual type: IO [Res a]
       NB: ‘Res’ is a type function, and may not be injective
     • In the expression: withDB $ query (select table :: Query s a)
       In an equation for ‘list’:
           list table = withDB $ query (select table :: Query s a)
     • Relevant bindings include
         table :: Table a (bound at src/Hedger/Backend.hs:30:6)
         list :: Table a -> IO [Res (Cols s a)]
           (bound at src/Hedger/Backend.hs:30:1)
    |
30 | list table = withDB $ query (select table :: Query s a)

  Couldn't match type ‘a’ with ‘Cols s a’
       ‘a’ is a rigid type variable bound by
         the type signature for:
           list :: forall s a.
                   (Result (Cols s a), Columns (Cols s a)) =>
                   Table a -> IO [Res (Cols s a)]
         at src/Hedger/Backend.hs:29:1-93
       Expected type: Query s a
         Actual type: Query s (Cols s a)
     • In the first argument of ‘query’, namely
         ‘(select table :: Query s a)’
       In the second argument of ‘($)’, namely
         ‘query (select table :: Query s a)’
       In the expression: withDB $ query (select table :: Query s a)
     • Relevant bindings include
         table :: Table a (bound at src/Hedger/Backend.hs:30:6)
         list :: Table a -> IO [Res (Cols s a)]
           (bound at src/Hedger/Backend.hs:30:1)
    |
30 | list table = withDB $ query (select table :: Query s a)
```

> -- or,                  ... (select @s table)
> -- with {-# LANGUAGE TypeApplications #-}
> ```

This indeed works!!

In either case, however, I need to add `{-# LANGUAGE FlexibleContexts #-}`

Now I have an interesting road in front of me in order to try to
understand it, along with Tom Ellis' isolated reproducing environment :)

Marc Busqué
http://waiting-for-dev.github.io/about/
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.