# Is it linear? - Haskell

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

Would this function typecheck with `-XLinear` enabled?

``````foo :: (Int -> ()) ⊸ ()
foo f = f 0 `seq` f 1
``````
``````GHCi, version 8.11.0.20200331: https://www.haskell.org/ghc/  :? for help
λ> :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,)
``````

(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

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

which says:

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

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

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

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

Alright, I guess it's `seq`:

``````λ> :t seq
seq :: a -> b -> b
``````

oh. can we define a linearly typed `seq`?

well, we can specialize it anyway

``````seq' :: () -> () -> ()
``````
``````seq' :: a #-> b #-> b
seq' = unsafeCoerce seq
``````

:stuck_out_tongue_wink:

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

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 consuming

so with this:

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

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

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:

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

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:

``````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
``````

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.

@Daniel Díaz Carrete aha, that makes sense

I wanted to know if Linear Type were supported in Haskell, I found this thread so it looks like it's the case. Is there some doc on the linear type extension ?