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

17 Mar 2016


      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,  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  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@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe