CODEWITHSUNDEEP
f#
user3587180
user3587180

Reputation: 1397

Why does the parameter b have a type a in this example?

I'm looking into aether library and noticed this

 type Lens<'a,'b> =
    ('a -> 'b) * ('b -> 'a -> 'a)

 static member (^=) (Set, (_, s): Lens<'a,'b>) =
            fun (b: 'b) ->
                s b : 'a -> 'a

In the ^= function, b parameter if of type 'b in the lambda. However, in the lamda body, why is b type of 'a now?

Upvotes: 3

Views: 78

Answers (2)

Fyodor Soikin
Fyodor Soikin

Reputation: 80915

I think you're just misreading the syntax. The code s b : 'a -> 'a doesn't mean that b is of type 'a.

The right way to read it is to break it in two parts: the part before the colon is the expression, and the part after the colon is the type of that expression.

So the code s b : 'a -> 'a actually means that s b is of type 'a -> 'a. It doesn't say anything about types of s or b individually.

Upvotes: 4

Reed Copsey
Reed Copsey

Reputation: 564861

However, in the lamda body, why is b type of 'a now?

It is not.

b is an input which is typed 'b, as shown in fun (b: 'b) ->.

We can rewrite that member without the matches, and using a locally defined function, like so:

static member (^=) (Set, lens: Lens<'a,'b>) =
    // Pattern match to extract out the 2nd portion of the lens, which is a function: 'b -> 'a -> 'a
    let (_,s) = lens

    // Define a function that takes a 'b and returns a new function of type: 'a -> 'a
    let fn (b: 'b) : 'a -> 'a =
        s b // this just partially applies s with the input "b"
    fn // Return the function

Basically, the (Set, (_,s)) in the argument list binds "s" to the 2nd portion of a Lens<'a,'b>, or a function typed ('b -> 'a -> 'a). Above, I've broken that out to be more explicit, and done this extraction in its own binding.

The member then returns a locally defined function (as a lambda). Above, I rewrote that using a let bound function, as it's often more clear.

Upvotes: 4

Related Questions