Welcome to linear-base Discussions!

[aspiwack]

👋 Welcome!

We’re using Discussions as a place to connect with other members of our community. We hope that you:

• Ask questions you’re wondering about.
• Share ideas.
• Engage with other community members.
• Welcome others and are open-minded. Remember that this is a community we
  build together 💪.

To get started, comment below with an introduction of yourself and tell us about what you do with this community.

[alt-romes]

Hello 👋

I got into linear types during my bachelor thesis where I started doing synthesis from linear types as specifications

Currently, I'm two weeks from finishing my master thesis on typing linearity in the presence of laziness, I'll keep you posted.

I've also developed a game engine (ghengin) whose core is entirely written in the linear IO monad

I'm looking forward to linear constraints in Haskell!

[aspiwack]

I'm looking forward to linear constraints in Haskell!

When I finish the linear let (which has been surprisingly hard, but should mostly be over now, I hope), I'll get on to make a GHC proposal for that. I don't have a ton of time, so progress is slow.

I've also developed a game engine (ghengin) whose core is entirely written in the linear IO monad

Impressive. How's your experience so far?

[joha2nes]

Hi!

I'm using Haskell on my spare time and got a bit interested in linear types mainly for predictable performance and its usability in Haskell. Linear types are still very new to me.

I wanted to do a test on using linear mutable arrays in real-time simulations and therefore need to read and write to the array at some point in within the IO monad. The only ways I found to create arrays in linear-base is using alloc, fromList and allocBeside. Especially alloc and fromList where you use the scoped function Movable b => (Array a %1 -> b). However, I don't see how I could use the array linearly in a monad since the linear IO monad (and StateT) isn't an instance of Movable.

What's the status on this? Is it possible to achieve what I'm aiming for or is there some limitations of linear types and linear-base that makes this unfeasible?

[aspiwack]

Hi @joha2nes ,

I guess we never got around to making one, but something like allocIO :: Int -> a -> Linear.IO (Array a) would be absolutely valid a way to create an array. But as you point out, it can't be derived from the scoped pure functions.

I can just add the primitive and make a release, if it's helpful to you. There are related discussions in #468 and #130, if you're interested. (the better solution uses linear constraints, but this is not going to happen very fast)