[Haskell-cafe] Selda: confused about type signtures
Marc Busqué
marc at lamarciana.com
Sun Apr 22 18:21:11 UTC 2018
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é <marc at lamarciana.com> 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
> allbery.b at gmail.com ballbery at sinenomine.net
> unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net
>
>
More information about the Haskell-Cafe
mailing list