StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
primarykey
Id
12087428
data
AcceptedAnswerId
0
AnswerCount
0
ClosedDate
CommentCount
3
CommunityOwnedDate
CreationDate
2012-08-23T08:15:05.950
FavoriteCount
0
LastActivityDate
2012-08-23T08:20:19.977
LastEditDate
2012-08-23T08:20:19.977
LastEditorUserId
828361
OwnerUserId
828361
ParentId
12085260
PostTypeId
2
Score
11
ViewCount
0
LastEditorDisplayName
text
Body
Type inference is, by default, a guessing game. Haskell's surface syntax makes it rather awkward to be explicit about which types should instantiate a <code>forall</code>, even if you know what you want. This is a legacy from the good old days of Damas-Milner completeness, when ideas interesting enough to require explicit typing were simply forbidden. Let's imagine we're allowed to make type application explicit in patterns and expressions using an Agda-style <code>f {a = x}</code> notation, selectively accessing the type parameter corresponding to <code>a</code> in the type signature of <code>f</code>. Your <pre><code>idT = StateT $ \ s -> idT </code></pre> is supposed to mean <pre><code>idT {a = a}{m = m} = StateT $ \ s -> idT {a = a}{m = m} </code></pre> so that the left has type <code>C a a (StateT s m) r</code> and the right has type <code>StateT s (C a a m) r</code>, which are equal by definition of the type family and joy radiates over the world. But that's not the meaning of what you wrote. The "variable-rule" for invoking polymorphic things requires that each <code>forall</code> is instantiated with a fresh existential type variable which is then solved by unification. So what your code means is <pre><code>idT {a = a}{m = m} = StateT $ \ s -> idT {a = a'}{m = m'} -- for a suitably chosen a', m' </code></pre> The available constraint, after computing the type family, is <pre><code>C a a m ~ C a' a' m' </code></pre> but that doesn't simplify, nor should it, because there is no reason to assume <code>C</code> is injective. And the maddening thing is that the machine cares more than you about the possibility of finding a most general solution. You have a suitable solution in mind already, but the problem is to achieve communication when the default assumption is guesswork. There are a number of strategies which might help you out of this jam. One is to use data families instead. Pro: injectivity no problem. Con: structor. (Warning, untested speculation below.) <pre><code>class MonadPipe m where data C a b (m :: * -> *) r idT :: C a a m r (<-<) :: C b c m r -> C a b m r -> C a c m r instance (MonadPipe m) => MonadPipe (StateT s m) where data C a b (StateT s m) r = StateTPipe (StateT s (C a b m) r) idT = StateTPipe . StateT $ \ s -> idT StateTPipe (StateT f) <-< StateTPipe (StateT g) = StateTPipe . StateT $ \ s - f s <-< g s </code></pre> Another con is that the resulting data family is not automatically monadic, nor is it so very easy to unwrap it or make it monadic in a uniform way. I'm thinking of trying out a pattern for these things where you keep your type family, but define a newtype wrapper for it <pre><code>newtype WrapC a b m r = WrapC {unwrapC :: C a b m r} </code></pre> then use <code>WrapC</code> in the types of the operations to keep the typechecker on the right track. I don't know if that's a good strategy, but I plan to find out, one of these days. A more direct strategy is to use proxies, phantom types, and scoped type variables (although this example shouldn't need them). (Again, speculation warning.) <pre><code>data Proxy (a :: *) = Poxy data ProxyF (a :: * -> *) = PoxyF class MonadPipe m where data C a b (m :: * -> *) r idT :: (Proxy a, ProxyF m) -> C a a m r ... instance (MonadPipe m) => MonadPipe (StateT s m) where data C a b (StateT s m) r = StateTPipe (StateT s (C a b m) r) idT pp = StateTPipe . StateT $ \ s -> idT pp </code></pre> That's just a crummy way of making the type applications explicit. Note that some people use <code>a</code> itself instead of <code>Proxy a</code> and pass <code>undefined</code> as the argument, thus failing to mark the proxy as such in the type and relying on not accidentally evaluating it. Recent progress with <code>PolyKinds</code> may at least mean we can have just one kind-polymorphic phantom proxy type. Crucially, the <code>Proxy</code> type constructors are injective, so my code really is saying "same parameters here as there". But there are times when I wish that I could drop to the System FC level in source code, or otherwise express a clear manual override for type inference. Such things are quite standard in the dependently typed community, where nobody imagines that the machine can figure everything out without a nudge here and there, or that hidden arguments carry no information worth inspecting. It's quite common that hidden arguments to a function can be suppressed at usage sites but need to be made explicit within the definition. The present situation in Haskell is based on a cultural assumption that "type inference is enough" which has been off the rails for a generation but still somehow persists.
Tags
Title
singulars
PostAcceptedAnswerId
1. This table or related slice is empty.
PostParentId
1. PORecursive Type Families
 singulars
 PostTypePostTypeId
 PTQuestion
PostTypePostTypeId
1. PTAnswer
UserLastEditorUserId
1. USpigworker
UserOwnerUserId
1. USpigworker
plurals
PostLinksPostIdRelatedPostId
1. This table or related slice is empty.
PostLinksRelatedPostIdPostId
1. This table or related slice is empty.
PostsAcceptedAnswerId
1. This table or related slice is empty.
PostsParentIdCreationDate
1. This table or related slice is empty.
VotesPostIdCreationDate
1. VO
 singulars
 PostPostId
 PO
 UserUserId
 This table or related slice is empty.
 VoteTypeVoteTypeId
 VTUpMod
2. VO
 singulars
 PostPostId
 PO
 UserUserId
 This table or related slice is empty.
 VoteTypeVoteTypeId
 VTUpMod
3. VO
 singulars
 PostPostId
 PO
 UserUserId
 This table or related slice is empty.
 VoteTypeVoteTypeId
 VTUpMod
CommentsPostId

Querying!

Guidance

A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.