[Haskell-cafe] Stuck on a type family problem where kind inference fails
Oliver Charles
ollie at ocharles.org.uk
Fri Mar 18 15:37:40 UTC 2016
Fascinating! The mentions of bidirectional type checking remind me of this
recent paper - Sound and Complete Bidirectional Typechecking for
Higher-Rank Polymorphism and Indexed Types
<http://www.cs.bham.ac.uk/~krishnan/gadt.pdf> - is this similar to what
would be required in GHC? The suffix of "for higher-rank polymorphism"
makes me wonder if this doesn't require solving impredicativity, as that
seems like a massive can of worms.
I'll read the conclusion of your paper again to see if I can learn more
about that wrt GHC 8. I'd love to donate some engineering resources, but I
have a feeling this might all be a little over my head.
Anyway, thanks for the discussion - it's been very interesting, even if the
outcome is perhaps slightly disappointing in the immediate. Of course,
there are other approaches I can take if I add a few more limitations, such
as only working for one specific ordering of "features" (e.g., columns of
kind (Column (Null (Default k)))), and that's what I've switched over to
for now.
- Ollie
On Fri, Mar 18, 2016 at 3:28 PM Richard Eisenberg <eir at cis.upenn.edu> wrote:
> Well, the issue as reported is now fixed (validating soon; barring
> disaster, will push today).
>
> But it doesn't fully solve the problem because my fix allows you to
> declare a higher-kinded type family but not to write higher-kinded type
> family equations. To do this requires proper bidirectional type-checking in
> types. GHC 8 actually has some degree of bidirectional type-checking in
> types, but not quite enough to pull this off. No real barriers here, just
> engineering time that I don't currently have. However, even if we had all
> the bidirectional type-checking and the ability to define higher-kinded
> type family equations, it *still* wouldn't work for you because the
> defunctionalization trick would fail. Defunctionalizing a higher-kinded
> type family requires impredicativity. (Think of the instantiation of the
> kind variables on the Apply function.) I'm not going to touch type-level
> impredicativity until term-level impredicativity is all sorted, and that is
> far from happening.
>
> The silver lining here is that I have an approach to unsaturated type
> functions (summarized in the conclusion to my paper about promoting
> functions to type families that describes the defunctionalization trick) in
> mind that will obviate the need for defunctionalization. My guess is that
> unsaturated type functions will be available before impredicativity, but I
> can't be sure.
>
> So, unbeknownst to you, your example requires a fair bit of research to be
> done before it can be written, in Haskell at least.
>
> Richard
>
> On Mar 18, 2016, at 10:26 AM, Richard Eisenberg <eir at cis.upenn.edu> wrote:
>
> Perhaps. On further consideration, this problem may not be as hard as I
> thought. I may get a chance to look into it today.
>
> On Mar 17, 2016, at 8:40 PM, Oliver Charles <ollie at ocharles.org.uk> wrote:
>
> 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
>>>>
>>>>
>>>>
>>>
> _______________________________________________
> 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/9871f5c9/attachment.html>
More information about the Haskell-Cafe
mailing list