[solved] Type inference question

Learn
#1

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
#2

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
#3

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
#4

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