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,)

λ> 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,)

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

Would this function typecheck with

`-XLinear`

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

That's about what I expected, but why?

Technically you're passing

`f`

in twice - and`seq`

would be`a -o b -> b`

, wouldn't it?sorry, I'm passing

`f`

in twice to what?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

which says:

what it doesn't say is "applying it

exactly once", even though it does say something like that in the data value caseSo I apply

`f`

two times, and each time I consume its result exactly once AFAICT, no?Hmm...:

Alright, I guess it's

`seq`

:oh. can we define a linearly typed

`seq`

?well, we can specialize it anyway

:stuck_out_tongue_wink:

does it work without unsafeCoerce if we just use

`()`

? i actually think it's wrong for it to be linear generallyunless you use deepSeq

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

yeah, if you make it parametric

`a`

could be a function or data type which you're not consumingso with this:

does it end up being linear?

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`

TheMatten said:

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

DURRRRRR it's

`-XLinearTypes`

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

but I don't quite get why

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

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

maybe because it returns unit :sweat_smile:

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

sounds reasonable

@Daniel Díaz Carrete aha, that makes sense