Pure "abc" -- what is the type?

#1 
PSCi, version 0.15.4
Type :? for help
import Prelude
import Effect.Console (log)
> x = pure "abc"
> :t x
forall (f1 :: Type -> Type). Applicative f1 => f1 String
> bind x log
abc

To improve my understanding of Applicative and Bind, I would like to know how to determine what the compiler used for f1.

Regards,
Mark

#2

It hasn’t used anything yet, rather it has quantified it. You can think of the forall and constraint as function arguments. Since it doesn’t know, it creates two new function arguments for the type f1 and the Applicative dictionary. If you were to try and use this in the future, the compiler would use inference to fill in these arguments with an appropriate type and solved Applicative dictionary.

#3

Ok, at the point of :t that is true but the question I was trying to ask can be better asked and answered by:

> x = pure "abc"
> bind (x :: ?f1_String) log
Error found:
in module $PSCI
at :1:12 - 1:22 (line 1, column 12 - line 1, column 22)

  Hole 'f1_String' has the inferred type
                 
    Effect String

Then I tried

f = \s → [s]
bind x f

and got

Array String for the type of the hole (i.e. f1 == Array)

Ok, things make sense. I will leave it.

1 Like