[Haskell-cafe] Stuck on a type family problem where kind inference fails

[Oliver Charles]

Your term level stuff is exactly what I got to - a need for rank-2 type..
Err, kinds! I was trying to do that within a class but gave up on GHC 7.
Great to hear GHC 8 will get me there, is there anything I can look at in
the mean time? I don't need singletons entirely, so I'm happy to
reimplement small parts.

- Ollie

On Thu, 17 Mar 2016 7:05 pm Richard Eisenberg, <eir at cis.upenn.edu> wrote:

> Interesting use case!
>
> You need a higher-rank kind.
>
> All the typey stuff is getting in the way of understanding. I've
> implemented what you want at the term level:
>
> data Null a = Nullable a | NotNullable a
>
> notNullableType :: (forall a. a -> Type) -> Null a -> Type
>
> notNullableType k (NotNullable a) = baseType k a
>
> nullableType :: (forall a. a -> Type) -> Null a -> Type
>
> nullableType k (Nullable a) = baseType (k . Nullable) a
>
> baseType :: (forall a. a -> Type) -> forall b. b -> Type
>
> baseType k a = k a
>
> exprTyFun :: Null b -> (forall a. a -> Type) -> Null b -> Type
> exprTyFun (NotNullable _) = notNullableType
> exprTyFun (Nullable _) = nullableType
>
>
> It's critical that notNullableType and nullableType have the same type,
> which is achievable only with higher-rank types.
>
> Happily, GHC 8.0 comes equipped with higher-rank kinds. `singletons`
> doesn't yet build on 8.0, but it will in the future, for a sufficiently
> expansive definition of future. Christiaan Baaij is working on this, but
> I've been all-consumed by getting GHC 8 out and haven't given Christiaan's
> contributions the attention they deserve. So: all in good time!
>
> I hope this answers your question.
>
> Richard
>
> On Mar 17, 2016, at 8:46 AM, Oliver Charles <ollie at ocharles.org.uk> wrote:
>
> Hi all,
>
> This is a little tricky to explain, so bear with me. I'm working on some
> code that roughly models a PostgreSQL schema. Users begin by defining their
> tables as Haskell records, parametrized over some f :: k -> *, and use a
> special Col type family that applies some normalisation:
>
> data Table f = Table { tableId :: Col f ('NotNullable 'DBInt)
>                      , tableX :: Col f ('Nullable 'DBString) }
>
> is one such example.
>
> The idea behind Col is that sometimes we don't need information about the
> "full type" when we know more about f.
>
> One such choice of f is Expr, which corresponds to expressions inside a
> query. In this case, I would desire
>
> tableId :: Col Expr ('NotNullable 'DBInt)  =  tableId :: Expr 'DBInt
> tableX :: Col Expr ('Nullable 'DBString)   =  tableX :: Expr ('Nullable
> 'DBString)
>
> Notice here that if you use 'NotNullable, then this information is erased
> - but it's important if the column is 'Nullable.
>
> However, I'm struggling to work out any way to actually pull this off in
> the general case. Here's what I've been attempting:
>
> {-# LANGUAGE FunctionalDependencies #-}
> {-# LANGUAGE FlexibleInstances #-}
> {-# LANGUAGE RankNTypes #-}
> {-# LANGUAGE MultiParamTypeClasses #-}
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE TypeOperators #-}
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE KindSignatures #-}
> {-# LANGUAGE PolyKinds #-}
> {-# LANGUAGE TemplateHaskell #-}
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE UndecidableInstances #-}
> {-# LANGUAGE ScopedTypeVariables #-}
>
> module ExprTest where
>
> import Data.Singletons
> import Data.Singletons.Prelude hiding (Null)
> import Data.Singletons.TH <http://data.singletons.th/>
>
> data Expr (a :: k)
>
> data MyExprSym :: TyFun k * -> *
> type instance Apply MyExprSym (x :: k) = Expr x
>
> $(singletons [d|
>   data Null a = Nullable a | NotNullable a
>   |])
>
> $(promote [d|
>   notNullableType k (NotNullable a) = baseType k a
>   nullableType k (Nullable a) = baseType (k . Nullable) a
>   baseType k a = k a
>   |])
>
> So far, this seems to work well. If I ask GHCI:
>
> *ExprTest> :kind! Apply (Apply NullableTypeSym0 MyExprSym) ('Nullable
> 'DBString)
> Apply (Apply NullableTypeSym0 MyExprSym) ('Nullable 'DBString) :: *
> = Expr ('Nullable 'DBString)
>
> *ExprTest> :kind! Apply (Apply NotNullableTypeSym0 MyExprSym)
> ('NotNullable 'DBInt)
> Apply (Apply NotNullableTypeSym0 MyExprSym) ('NotNullable 'DBInt) :: *
> = Expr 'DBInt
>
> This is exactly what I want, but note that I had to choose the necessary
> symbols NullableTypeSym0 and NotNullableTypeSym0. I would like to
> calculate those symbols from the column type itself. Looking at the kinds
> of these symbols though, they are both different:
>
> *ExprTest> :kind! NotNullableTypeSym0
> NotNullableTypeSym0 :: TyFun
>                          (TyFun k1 k -> *) (TyFun (Null k1) k -> *)
>                        -> *
> = NotNullableTypeSym0
> *ExprTest> :kind! NullableTypeSym0
> NullableTypeSym0 :: TyFun
>                       (TyFun (Null k1) k -> *) (TyFun (Null k1) k -> *)
>                     -> *
> = NullableTypeSym0
>
> So I can't see a way to write a single type family that returns them.
>
>
> To summarise, I'd like a way to write this following instance for Col:
>
> type instance Col Expr x = Apply (Apply ?? MyExprSym) x
>
> such that
>
> Col Expr ('Nullable a) = Expr ('Nullable a') and
> Col Expr ('NotNullable a) = Expr a
>
> but I cannot work out how to write the placeholder ?? above.
>
> One attempt is
>
> type family ExprTyfun (col :: colK) :: TyFun (TyFun k * -> *) (TyFun j *
> -> *) -> *
> type instance ExprTyfun ('NotNullable a) = NotNullableTypeSym0
> type instance ExprTyfun ('Nullable a) = NullableTypeSym0
>
> But neither of these instances actually normalise as I'd like, presumably
> because of k and j being forall'd in the return type:
>
> *ExprTest> :set -fprint-explicit-kinds
>
>
> *ExprTest> :kind! ExprTyfun ('Nullable 'DBInt)
> ExprTyfun ('Nullable 'DBInt) :: TyFun
>                                   (TyFun k * -> *) (TyFun k1 * -> *)
>                                 -> *
> = ExprTyfun k k1 (Null DBType) ('Nullable DBType 'DBInt)
>
>
> *ExprTest> :kind! ExprTyfun ('NotNullable 'DBInt)
> ExprTyfun ('NotNullable 'DBInt) :: TyFun
>                                      (TyFun k * -> *) (TyFun k1 * -> *)
>                                    -> *
> = ExprTyfun k k1 (Null DBType) ('NotNullable DBType 'DBInt)
>
>
> *ExprTest> :i ExprTyfun
> type family ExprTyfun (k :: BOX)
>                       (j :: BOX)
>                       (colK :: BOX)
>                       (col :: colK) ::
>   TyFun (TyFun k * -> *) (TyFun j * -> *) -> *
>   -- Defined at src/Opaleye/TF/ExprTest.hs:39:1
> type instance ExprTyfun
>                 (Null k) (Null k) (Null k1) ('Nullable k1 a)
>   = NullableTypeSym0 * k
>   -- Defined at src/Opaleye/TF/ExprTest.hs:41:1
> type instance ExprTyfun k (Null k) (Null k1) ('NotNullable k1 a)
>   = NotNullableTypeSym0 * k
>   -- Defined at src/Opaleye/TF/ExprTest.hs:40:1
>
>
> I'd also like to point out that in my full code the types to Col can be a
> lot bigger, and I'd like to not assume any ordering. For example, here's a
> possible type:
>
>   userId :: Col f ('Column "id" ('NotNullable ('HasDefault 'DBInt)))
>
> In this case Col Expr ('Column "id" ('NotNullable ('HasDefault 'DBInt)))
> = Expr 'DBInt
>
> I hope this question is understandable! Please let me know if there's
> anything I can do to provide more clarity.
>
> - Ollie
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160317/36a48669/attachment.html>