# 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,)
`````` Technically you're passing `f` in twice - and `seq` would be `a -o b -> b`, wouldn't it? 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
`````` does it work without unsafeCoerce if we just use `()`? i actually think it's wrong for it to be linear generally 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` oh, I see. I guess linear types being merged doesn't necessarily equate to being available for use yet 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
`````` 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"." Intuitively, I would find weird if a function "that can be used once" could be applied two times. 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 ?