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

Richard Eisenberg eir at cis.upenn.edu
Mon Mar 21 21:42:27 UTC 2016 

On Mar 18, 2016, at 11:37 AM, Oliver Charles <ollie at ocharles.org.uk> wrote:

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

The Dunfield/Krishnaswami papers have a key detail that makes them fall short of what we need in GHC: let-generalization. The type system in that paper is, if my understanding is correct, not an extension of Hindley-Milner.

When I say bidirectional typechecking here, I mean something like the "Practical Type Inference for Higher-Rank Types" paper or my recent "Visible Type Application" paper.

I hope this helps!
Richard

> 
> 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
>>>>> 
>>>>> 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/20160321/09368b41/attachment.html>

More information about the Haskell-Cafe mailing list