[solved] Type inference question

Hello everyone,

I came across a type example from a book that I found to be quite complex.

``````data Stream f m r = Step (f (Stream f m r))
| Effect (m (Stream f m r))
| Return r
data Of a b = a :> b
deriving Show

empty :: Stream f m ()
empty = Return ()
``````
``````*Main> a = 1 :> empty
*Main> :t a
a :: Num a => Of a (Stream f m ()) -- Got it. Understood
*Main> b = Step a
*Main> :t b
b :: Num a => Stream (Of a) m ()  -- Seems cryptic.
*Main>
``````

The type constructor `Step` belongs to the `Stream` data type, so I expected the resulting type to be `Stream A B C`. The format of the type, which is `Stream (Of a) m ()`, seems to be correct. However, I am having difficulty understanding why the `Of a` is added to `A`, `m` is added to `B`, and `()` is added to `C` by the compiler. Can someone please help me understand how this works? Thank you.

1 Like

Since you agree `a :: Of a (Stream f m ())` aka `(Of a) (Stream f m ())`, and `Step` wants its field type to take the form `g (Stream g n r)`, we need to use change some letters because we don’t yet know whether g will be f, n will be m (we’ll find out soon), let’s do a matching up shall we?

``````(Of a) (Stream f m ())
g    (Stream g n r )
``````

So g has to be `Of a`, f has to be g so f is also `Of a`, r has to be `()`. m and n have to be the same afterall, but otherwise we know nothing, let’s arbitrarily call them m.

With that, the type of `Step a` takes the form `Stream g n r` but we have solved for g, n, and r, so it becomes `Stream (Of a) m ()`.

4 Likes

Thank you for your response! Unfortunately, I can’t seem to locate the answer mark in my view, so I clicked the ‘like’ button instead. Thank you again for your help.

3 Likes

We don’t have a way to mark answers yet, but it has been suggested:

For now I’ve just added [solved] to the title.

3 Likes