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
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 ?
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 - andseq
would bea -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 case
So 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
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 ?
https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/exts/linear_types.html#extension-LinearTypes
thank you !
Another nice intro https://tek.brick.do/EGnqyrBDQ5Gk