Is it linear? - Haskell

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Asad Saeeduddin

Would this function typecheck with -XLinear enabled?

foo :: (Int -> ())  ()
foo f = f 0 `seq` f 1
TheMatten
GHCi, version 8.11.0.20200331: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/matej/.ghci
λ> :set -XLinearTypes -XUnicodeSyntax
λ> foo :: (Int -> ()) ⊸ (); foo f = f 0 `seq` f 1

<interactive>:7:30: error:
    • Couldn't match type ‘'Many’ with ‘'One’
        arising from multiplicity of ‘f’
    • In an equation for ‘foo’: foo f = f 0 `seq` f 1
(0.01 secs,)
TheMatten

(It's the older fork though, not sure if something changed in GHC HEAD)

Asad Saeeduddin

That's about what I expected, but why?

TheMatten

Technically you're passing f in twice - and seq would be a -o b -> b, wouldn't it?

Asad Saeeduddin

sorry, I'm passing f in twice to what?

Asad Saeeduddin

The definition I've been trying to understand this in terms of is: https://github.com/tweag/ghc-proposals/blob/6edfe1b836036755f8d48886639434b92fc90344/proposals/0000-linear-types.rst#31definition

Proposed compiler and language changes for GHC and GHC/Haskell - tweag/ghc-proposals
Asad Saeeduddin

which says:

Consuming a function exactly once means applying it and consuming its result exactly once

Asad Saeeduddin

what it doesn't say is "applying it exactly once", even though it does say something like that in the data value case

Asad Saeeduddin

So I apply f two times, and each time I consume its result exactly once AFAICT, no?

TheMatten

Hmm...:

λ> foo :: (Int -> ()) ⊸ (); foo f = () `seq` f 1

<interactive>:8:30: error:
    • Couldn't match type ‘'Many’ with ‘'One’
        arising from multiplicity of ‘f’
    • In an equation for ‘foo’: foo f = () `seq` f 1
(0.01 secs,)
λ> foo :: (Int -> ()) ⊸ (); foo f = f 0 `seq` ()

<interactive>:9:30: error:
    • Couldn't match type ‘'Many’ with ‘'One’
        arising from multiplicity of ‘f’
    • In an equation for ‘foo’: foo f = f 0 `seq` ()
(0.01 secs,)
TheMatten

Alright, I guess it's seq:

λ> :t seq
seq :: a -> b -> b
Asad Saeeduddin

oh. can we define a linearly typed seq?

Asad Saeeduddin

well, we can specialize it anyway

Asad Saeeduddin
seq' :: () -> () -> ()
TheMatten
seq' :: a #-> b #-> b
seq' = unsafeCoerce seq

:stuck_out_tongue_wink:

Asad Saeeduddin

does it work without unsafeCoerce if we just use ()? i actually think it's wrong for it to be linear generally

TheMatten

Hmm - like that it doesn't consume it's fields?

Asad Saeeduddin

yeah, if you make it parametric a could be a function or data type which you're not consuming

Asad Saeeduddin

so with this:

seq' :: () ⊸ () ⊸ ()
seq' () () = ()

foo :: (Int -> ()) ⊸ ()
foo f = f 0 `seq'` f 1

does it end up being linear?

Asad Saeeduddin

How are you actually getting -XLinear btw? I'm building GHC master (I think) and I still only get 8.11.0.2020701, with no -XLinear

Georgi Lyubenov // googleson78

TheMatten said:

(It's the older fork though, not sure if something changed in GHC HEAD)

Asad Saeeduddin

oh, I see. I guess linear types being merged doesn't necessarily equate to being available for use yet

Asad Saeeduddin

DURRRRRR it's -XLinearTypes

Asad Saeeduddin

Ok, so it's actually not linear, I get:

Prelude> foo :: (Int -> ()) #-> (); foo f = f 0 `seq'` f 1

<interactive>:23:32: error:
    • Couldn't match type ‘'Many’ with ‘'One’
        arising from multiplicity of ‘f’
    • In an equation for ‘foo’: foo f = f 0 `seq'` f 1
Asad Saeeduddin

but I don't quite get why

Daniel Díaz Carrete

Pehaps "consuming a function exactly once means (applying it and consuming its result) exactly once".

Daniel Díaz Carrete

or "consuming a function exactly once means (applying it and consuming its result exactly once) exactly once"."

Torsten Schmits

maybe because it returns unit :sweat_smile:

Daniel Díaz Carrete

Intuitively, I would find weird if a function "that can be used once" could be applied two times.

Asad Saeeduddin

@Daniel Díaz Carrete aha, that makes sense