<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; "><div>Yes, please do, with your use case. These examples are very helpful!</div><div><br></div><div>Thanks,</div><div>Richard</div><br><div><div>On Mar 17, 2016, at 4:29 PM, Oliver Charles <<a href="mailto:ollie@ocharles.org.uk">ollie@ocharles.org.uk</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><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">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><br></body></html>