[Haskell-cafe] Stuck on a type family problem where kind inference fails
Oliver Charles
ollie at ocharles.org.uk
Fri Mar 18 00:40:49 UTC 2016
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 at ocharles.org.uk>
wrote:
> Rats. Shall I open something in Trac?
>
> On Thu, 17 Mar 2016 8:26 pm Richard Eisenberg, <eir at 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 at 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 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/20160318/42d88f04/attachment.html>
More information about the Haskell-Cafe
mailing list