<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><br><div><div>On Mar 18, 2016, at 11:37 AM, Oliver Charles <<a href="mailto:ollie@ocharles.org.uk">ollie@ocharles.org.uk</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div dir="ltr">Fascinating! The mentions of bidirectional type checking remind me of this recent paper - <a href="http://www.cs.bham.ac.uk/~krishnan/gadt.pdf" style="color:rgb(77,70,156);font-family:Arial,Tahoma,Helvetica,FreeSans,sans-serif;line-height:18.2px">Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism and Indexed Types</a> - 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.</div></blockquote><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>I hope this helps!</div><div>Richard</div><br><blockquote type="cite"><div dir="ltr"><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>- Ollie</div></div><br><div class="gmail_quote"><div dir="ltr">On Fri, Mar 18, 2016 at 3:28 PM Richard Eisenberg <<a href="mailto:eir@cis.upenn.edu">eir@cis.upenn.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div>Well, the issue as reported is now fixed (validating soon; barring disaster, will push today).</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>So, unbeknownst to you, your example requires a fair bit of research to be done before it can be written, in Haskell at least.</div></div><div style="word-wrap:break-word"><div><br></div><div>Richard</div></div><div style="word-wrap:break-word"><br><div><div>On Mar 18, 2016, at 10:26 AM, Richard Eisenberg <<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>> wrote:</div><br><blockquote type="cite"><div style="word-wrap:break-word"><div>Perhaps. On further consideration, this problem may not be as hard as I thought. I may get a chance to look into it today.</div><br><div><div>On Mar 17, 2016, at 8:40 PM, Oliver Charles <<a href="mailto:ollie@ocharles.org.uk" target="_blank">ollie@ocharles.org.uk</a>> wrote:</div><br><blockquote type="cite"><div dir="ltr">I have just found <a href="https://ghc.haskell.org/trac/ghc/ticket/11635" target="_blank">https://ghc.haskell.org/trac/ghc/ticket/11635</a> - is that perhaps the same thing?</div><br><div class="gmail_quote"><div dir="ltr">On Thu, Mar 17, 2016 at 8:29 PM Oliver Charles <<a href="mailto:ollie@ocharles.org.uk" target="_blank">ollie@ocharles.org.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><p dir="ltr">Rats. Shall I open something in Trac?</p>
<br><div class="gmail_quote"><div dir="ltr">On Thu, 17 Mar 2016 8:26 pm Richard Eisenberg, <<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div>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.</div><div><br></div><div>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.</div><div><br></div><div>Just to show what I tried:</div><div><br></div><div><div></div></div><blockquote type="cite"><div>import Data.Kind</div><div><br></div><div>data TyFun :: * -> * -> *</div><div>type a ~> b = TyFun a b -> *</div><div><br></div><div>type family (f :: a ~> b) @@ (x :: a) :: b</div></blockquote></div><div style="word-wrap:break-word"><blockquote type="cite"><div><br></div><div>data Null a = Nullable a | NotNullable a</div><div><br></div></blockquote></div><div style="word-wrap:break-word"><blockquote type="cite"><div>type family ((f :: b ~> c) ∘ (g :: a ~> b)) (x :: a) :: c where</div><div> (f ∘ g) x = f @@ (g @@ x)</div><div><br></div></blockquote><blockquote type="cite"><div>type family BaseType (k :: forall a. a ~> Type) (x :: b) :: Type where -- this fails :(</div><div>-- BaseType k x = (@@) k x</div></blockquote><div><br></div><div>(By the way, Type and * are synonyms in GHC 8. There's no rhyme nor reason for why I used both in this example.)</div></div><div style="word-wrap:break-word"><div><br></div><div>Richard</div></div><div style="word-wrap:break-word"><br><div><div>On Mar 17, 2016, at 4:12 PM, Oliver Charles <<a href="mailto:ollie@ocharles.org.uk" target="_blank">ollie@ocharles.org.uk</a>> wrote:</div><br><blockquote type="cite"><p dir="ltr">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.</p><p dir="ltr">- Ollie</p>
<br><div class="gmail_quote"><div dir="ltr">On Thu, 17 Mar 2016 7:05 pm Richard Eisenberg, <<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div>Interesting use case!</div><div><br></div><div>You need a higher-rank kind.</div><div><br></div><div>All the typey stuff is getting in the way of understanding. I've implemented what you want at the term level:</div><div><br></div><div><div></div><blockquote type="cite"></blockquote></div></div><div style="word-wrap:break-word"><blockquote type="cite"><div>data Null a = Nullable a | NotNullable a</div><div><br></div></blockquote></div><div style="word-wrap:break-word"><blockquote type="cite">notNullableType :: (forall a. a -> Type) -> Null a -> Type</blockquote></div><div style="word-wrap:break-word"><blockquote type="cite"><div>notNullableType k (NotNullable a) = baseType k a</div><div><br></div></blockquote></div><div style="word-wrap:break-word"><blockquote type="cite">nullableType :: (forall a. a -> Type) -> Null a -> Type</blockquote></div><div style="word-wrap:break-word"><blockquote type="cite"><div>nullableType k (Nullable a) = baseType (k . Nullable) a</div><div><br></div></blockquote></div><div style="word-wrap:break-word"><blockquote type="cite">baseType :: (forall a. a -> Type) -> forall b. b -> Type</blockquote></div><div style="word-wrap:break-word"><blockquote type="cite"><div>baseType k a = k a</div><div><br></div></blockquote></div><div style="word-wrap:break-word"><div><blockquote type="cite"><div>exprTyFun :: Null b -> (forall a. a -> Type) -> Null b -> Type</div><div>exprTyFun (NotNullable _) = notNullableType</div><div>exprTyFun (Nullable _) = nullableType</div></blockquote></div><div><br></div><div>It's critical that notNullableType and nullableType have the same type, which is achievable only with higher-rank types.</div><div><br></div><div>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!</div><div><br></div><div>I hope this answers your question.</div><div><br></div><div>Richard</div><br><div></div></div><div style="word-wrap:break-word"><div>On Mar 17, 2016, at 8:46 AM, Oliver Charles <<a href="mailto:ollie@ocharles.org.uk" target="_blank">ollie@ocharles.org.uk</a>> wrote:</div><br></div><div style="word-wrap:break-word"><blockquote type="cite"><div dir="ltr">Hi all,<div><br></div><div>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 <font face="monospace, monospace">f :: k -> *</font>, and use a special <font face="monospace, monospace">Col</font> type family that applies some normalisation:</div><div><br></div><div><font face="monospace, monospace">data Table f = Table { tableId :: Col f ('NotNullable 'DBInt)</font></div><div><font face="monospace, monospace"> , tableX :: Col f ('Nullable 'DBString) }</font></div><div><br></div><div>is one such example.</div><div><br></div><div>The idea behind <font face="monospace, monospace">Col</font> is that sometimes we don't need information about the "full type" when we know more about <font face="monospace, monospace">f</font>.</div><div><br></div><div>One such choice of <font face="monospace, monospace">f</font> is <font face="monospace, monospace">Expr</font>, which corresponds to expressions inside a query. In this case, I would desire</div><div><br></div><div><font face="monospace, monospace">tableId :: Col Expr ('NotNullable 'DBInt) = tableId :: Expr 'DBInt</font></div><div><font face="monospace, monospace">tableX :: Col Expr ('Nullable 'DBString) = tableX :: Expr ('Nullable 'DBString)</font></div><div><br></div><div>Notice here that if you use <font face="monospace, monospace">'NotNullable</font>, then this information is erased - but it's important if the column is <font face="monospace, monospace">'Nullable</font>.</div><div><br></div><div>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:</div><div><br></div><div><div><font face="monospace, monospace">{-# LANGUAGE FunctionalDependencies #-}</font></div><div><font face="monospace, monospace">{-# LANGUAGE FlexibleInstances #-}</font></div><div><font face="monospace, monospace">{-# LANGUAGE RankNTypes #-}</font></div><div><font face="monospace, monospace">{-# LANGUAGE MultiParamTypeClasses #-}</font></div><div><font face="monospace, monospace">{-# LANGUAGE DataKinds #-}</font></div><div><font face="monospace, monospace">{-# LANGUAGE TypeOperators #-}</font></div><div><font face="monospace, monospace">{-# LANGUAGE TypeFamilies #-}</font></div><div><font face="monospace, monospace">{-# LANGUAGE KindSignatures #-}</font></div><div><font face="monospace, monospace">{-# LANGUAGE PolyKinds #-}</font></div><div><font face="monospace, monospace">{-# LANGUAGE TemplateHaskell #-}</font></div><div><font face="monospace, monospace">{-# LANGUAGE GADTs #-}</font></div><div><font face="monospace, monospace">{-# LANGUAGE UndecidableInstances #-}</font></div><div><font face="monospace, monospace">{-# LANGUAGE ScopedTypeVariables #-}</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">module ExprTest where</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">import Data.Singletons</font></div><div><font face="monospace, monospace">import Data.Singletons.Prelude hiding (Null)<br>import <a href="http://data.singletons.th/" target="_blank">Data.Singletons.TH</a></font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">data Expr (a :: k)</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">data MyExprSym :: TyFun k * -> *</font></div><div><font face="monospace, monospace">type instance Apply MyExprSym (x :: k) = Expr x</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">$(singletons [d|</font></div><div><font face="monospace, monospace"> data Null a = Nullable a | NotNullable a</font></div><div><font face="monospace, monospace"> |])</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">$(promote [d|</font></div><div><font face="monospace, monospace"> notNullableType k (NotNullable a) = baseType k a</font></div><div><font face="monospace, monospace"> nullableType k (Nullable a) = baseType (k . Nullable) a</font></div><div><font face="monospace, monospace"> baseType k a = k a</font></div><div><font face="monospace, monospace"> |])</font></div></div><div><br></div><div>So far, this seems to work well. If I ask GHCI:</div><div><br></div><div><div><font face="monospace, monospace">*ExprTest> :kind! Apply (Apply NullableTypeSym0 MyExprSym) ('Nullable 'DBString)</font></div><div><font face="monospace, monospace">Apply (Apply NullableTypeSym0 MyExprSym) ('Nullable 'DBString) :: *</font></div><div><font face="monospace, monospace">= Expr ('Nullable 'DBString)</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">*ExprTest> :kind! Apply (Apply NotNullableTypeSym0 MyExprSym) ('NotNullable 'DBInt)</font></div><div><font face="monospace, monospace">Apply (Apply NotNullableTypeSym0 MyExprSym) ('NotNullable 'DBInt) :: *</font></div><div><font face="monospace, monospace">= Expr 'DBInt</font></div></div><div><br></div><div>This is exactly what I want, but note that I had to choose the necessary symbols <font face="monospace, monospace">NullableTypeSym0</font> and <font face="monospace, monospace">NotNullableTypeSym0</font>. I would like to calculate those symbols from the column type itself. Looking at the kinds of these symbols though, they are both different:</div><div><br></div><div><div><font face="monospace, monospace">*ExprTest> :kind! NotNullableTypeSym0</font></div><div><font face="monospace, monospace">NotNullableTypeSym0 :: TyFun</font></div><div><font face="monospace, monospace"> (TyFun k1 k -> *) (TyFun (Null k1) k -> *)</font></div><div><font face="monospace, monospace"> -> *</font></div><div><font face="monospace, monospace">= NotNullableTypeSym0</font></div><div><font face="monospace, monospace">*ExprTest> :kind! NullableTypeSym0</font></div><div><font face="monospace, monospace">NullableTypeSym0 :: TyFun</font></div><div><font face="monospace, monospace"> (TyFun (Null k1) k -> *) (TyFun (Null k1) k -> *)</font></div><div><font face="monospace, monospace"> -> *</font></div><div><font face="monospace, monospace">= NullableTypeSym0</font></div></div><div><br></div><div>So I can't see a way to write a single type family that returns them.</div><div><br></div><div><br></div><div>To summarise, I'd like a way to write this following instance for Col:</div><div><br></div><div><font face="monospace, monospace">type instance Col Expr x = Apply (Apply ?? MyExprSym) x</font></div><div><br></div><div>such that </div><div><br></div><div><font face="monospace, monospace">Col Expr ('Nullable a) = Expr ('Nullable a')</font> and</div><div><font face="monospace, monospace">Col Expr ('NotNullable a) = Expr a</font></div><div><br></div><div>but I cannot work out how to write the placeholder ?? above.</div><div><br></div><div>One attempt is </div><div><br></div><div><div><font face="monospace, monospace">type family ExprTyfun (col :: colK) :: TyFun (TyFun k * -> *) (TyFun j * -> *) -> *</font></div><div><font face="monospace, monospace">type instance ExprTyfun ('NotNullable a) = NotNullableTypeSym0</font></div><div><font face="monospace, monospace">type instance ExprTyfun ('Nullable a) = NullableTypeSym0</font></div></div><div><br></div><div>But neither of these instances actually normalise as I'd like, presumably because of <font face="monospace, monospace">k</font> and <font face="monospace, monospace">j</font> being <font face="monospace, monospace">forall</font><font face="arial, helvetica, sans-serif">'d</font> in the return type:</div><div><br></div><div><div><font face="monospace, monospace">*ExprTest> :set -fprint-explicit-kinds</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"><br></font></div><div><span style="font-family:monospace,monospace">*ExprTest> :kind! ExprTyfun ('Nullable 'DBInt)</span><br></div><div><font face="monospace, monospace">ExprTyfun ('Nullable 'DBInt) :: TyFun</font></div><div><font face="monospace, monospace"> (TyFun k * -> *) (TyFun k1 * -> *)</font></div><div><font face="monospace, monospace"> -> *</font></div><div><font face="monospace, monospace">= ExprTyfun k k1 (Null DBType) ('Nullable DBType 'DBInt)</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">*ExprTest> :kind! ExprTyfun ('NotNullable 'DBInt)</font></div><div><font face="monospace, monospace">ExprTyfun ('NotNullable 'DBInt) :: TyFun</font></div><div><font face="monospace, monospace"> (TyFun k * -> *) (TyFun k1 * -> *)</font></div><div><font face="monospace, monospace"> -> *</font></div><div><font face="monospace, monospace">= ExprTyfun k k1 (Null DBType) ('NotNullable DBType 'DBInt)</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">*ExprTest> :i ExprTyfun</font></div><div><font face="monospace, monospace">type family ExprTyfun (k :: BOX)</font></div><div><font face="monospace, monospace"> (j :: BOX)</font></div><div><font face="monospace, monospace"> (colK :: BOX)</font></div><div><font face="monospace, monospace"> (col :: colK) ::</font></div><div><font face="monospace, monospace"> TyFun (TyFun k * -> *) (TyFun j * -> *) -> *</font></div><div><font face="monospace, monospace"> <span style="white-space:pre-wrap"> </span>-- Defined at src/Opaleye/TF/ExprTest.hs:39:1</font></div><div><font face="monospace, monospace">type instance ExprTyfun</font></div><div><font face="monospace, monospace"> (Null k) (Null k) (Null k1) ('Nullable k1 a)</font></div><div><font face="monospace, monospace"> = NullableTypeSym0 * k</font></div><div><font face="monospace, monospace"> <span style="white-space:pre-wrap"> </span>-- Defined at src/Opaleye/TF/ExprTest.hs:41:1</font></div><div><font face="monospace, monospace">type instance ExprTyfun k (Null k) (Null k1) ('NotNullable k1 a)</font></div><div><font face="monospace, monospace"> = NotNullableTypeSym0 * k</font></div><div><font face="monospace, monospace"> <span style="white-space:pre-wrap"> </span>-- Defined at src/Opaleye/TF/ExprTest.hs:40:1</font></div></div><div><br></div><div><br></div><div>I'd also like to point out that in my full code the types to <font face="monospace, monospace">Col</font> can be a lot bigger, and I'd like to not assume any ordering. For example, here's a possible type:</div><div><br></div><div> <font face="monospace, monospace">userId :: Col f ('Column "id" ('NotNullable ('HasDefault 'DBInt)))</font></div><div><br></div><div>In this case <font face="monospace, monospace">Col Expr ('Column "id" ('NotNullable ('HasDefault 'DBInt))) = Expr 'DBInt</font></div><div><br></div><div>I hope this question is understandable! Please let me know if there's anything I can do to provide more clarity.</div><div><br></div><div>- Ollie</div></div></blockquote></div><div style="word-wrap:break-word"><div><blockquote type="cite">
_______________________________________________<br>Haskell-Cafe mailing list<br><a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br></blockquote></div><br></div></blockquote></div>
</blockquote></div><br></div></blockquote></div></blockquote></div>
</blockquote></div><br></div>_______________________________________________<br>Haskell-Cafe mailing list<br><a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br></blockquote></div><br></div></blockquote></div>
</blockquote></div><br></body></html>