I have just found https://ghc.haskell.org/trac/ghc/ticket/11635 - is that perhaps the same thing?

On Thu, Mar 17, 2016 at 8:29 PM Oliver Charles <ollie@ocharles.org.uk> wrote:

Rats. Shall I open something in Trac?

On Thu, 17 Mar 2016 8:26 pm Richard Eisenberg, <eir@cis.upenn.edu> wrote:

Bah. I've just tried to mock something up, but GHC 8 doesn't support higher-rank kinds in type families. They work fine in datatypes and classes, but not in type families. I know exactly why this is failing, and I'm pretty sure I know how to fix it, but it's certainly not going to make it for GHC 8 -- there's a significant engineering hurdle before we can allow type family arguments' kinds to be fancy.

Sorry to disappoint here. Perhaps there's a way to work around the problem, maybe by burying the higher-rank kind under a newtype or some similar trick.

Just to show what I tried:

import Data.Kind

data TyFun :: * -> * -> *

type a ~> b = TyFun a b -> *

type family (f :: a ~> b) @@ (x :: a) :: b

data Null a = Nullable a | NotNullable a

type family ((f :: b ~> c) ∘ (g :: a ~> b)) (x :: a) :: c where

  (f ∘ g) x = f @@ (g @@ x)

type family BaseType (k :: forall a. a ~> Type) (x :: b) :: Type where   -- this fails :(

--  BaseType k x = (@@) k x

(By the way, Type and * are synonyms in GHC 8. There's no rhyme nor reason for why I used both in this example.)

Richard

On Mar 17, 2016, at 4:12 PM, Oliver Charles <ollie@ocharles.org.uk> wrote:

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@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@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

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