bjz_

It is, but they are not full spectrum dependent types, as far as I know. ATS doesn't have a Rust-style region system either, as far as I'm aware. It's very cool though, and quite inspiring, if a little unfriendly UX wise! :)

Yeah, I'm aware of Quantitative Type Theory, it's very cool! Another neat iteration is described in "Resourceful Dependent Types"[0]. I'm interested in what the Granule people are doing though - they can track usage information at the type level too. It's still non-dependent for now, but I hear that they are interested in extending it to dependent types too. They use an SMT solver to track usage information which is really neat - apparently it allows to track more interesting usage patterns than Blodwen can.

Sadly this doesn't do everything I want though - AFAIK, you can still have multiple out-standing references in linear typing [1]. I'd really like some story for uniqueness too in order to have support for in-place updates while avoiding a GC.

[0]: http://www2.tcs.ifi.lmu.de/~abel/talkTYPES18.pdf

[1]: https://en.wikipedia.org/wiki/Uniqueness_type#Relationship_t...

Mercury brings a bit more sanity to Prolog with its mode system. This is one of the key reasons why it runs fast and can be used to build big systems like Prince. That said, it _is_ a restriction on expressiveness of programs, and sometimes that makes it hard to do certain things. That's true of any type system.

There's still an interesting question about whether a different iteration on the mode system could capture more of the semantics of Prolog while still being useful, but so far nobody has done that research yet. It's more trendy to do FP research these days, so I'm expecting it could be a _long_ time before we get an answer, sadly.

Waaaaaat. There's so much in Haskell's type system that is also in logic programming. Like Hindley-Milner type inference and type class instance resolution.

> I'm sure this is awesome, but there's no code examples until I download a read a PDF tutorial.

Yeah, I definitely think this is something that could be improved - Mercury tends to come from a more 'old-school' form of OSS where the importance of marketing and design was less well understood. I hope they get around to fixing this!

The biggest thing that Mercury brings to the table is types, a mode system, and performance. This makes it viable for large scale software development.

Funnily enough we don't actually use the built-in non-determinism all that much. Often the layout tasks that HTML and CSS demand require us to build our own, bespoke algorithms, for performance and control reasons. We still get a bunch of leverage out of the type system and data modelling power of the language though.

I work at YesLogic and answered a similar question on Lobste.rs recently: https://lobste.rs/s/7op1vm/my_first_3_weeks_professional_rus...

The gist of it (as far as I understand it) is that at the time Prince was started (around 2003?), there wasn't a declarative/functional programming language out there to use that was fast enough, or had as much interest in low level control as Mercury had. The founders were pretty convinced that this was the style of programming they wanted to do, and the creators of Mercury were locals to Melbourne, so that kind of tipped things in Mercury's favor.

In general we tend to use the functional/typed parts of the language more than the logic parts of the language (although that can be handy at times). Pretty much any form of programming can benefit from being expressed in that way. It might be that the team is so highly competent, but the Prince source is one of the best I've seen, even after all these years, and it's still reasonably easy to make changes without fear. That's mainly what we get out of Mercury.

> A language with dependent types and borrow checking

I'm definitely interested in this! There are significant challenges here though, particularly with respect to combining dependent types with effects and coeffects! This is open research, but significant progress is being made, and I'm hopeful. I'm currently keeping an eye on https://github.com/granule-project/granule, which seems like it might have some interesting things to say about this.

Currently I'm trying to learn how to implement dependent types in my programming language, Pikelet: https://github.com/pikelet-lang/pikelet (currently doing a rebuild of the front-end in https://github.com/brendanzab/rust-nbe-for-mltt). I'm hoping that once I've done this I might eventually be able to start looking at implementing something to do with borrow checking in it, but who knows! The more I learn the less I seem to know! Always interested in chatting to people about this at our Gitter channel: https://gitter.im/pikelet-lang/Lobby

> Idris is perhaps the most famous dependently typed language.

I'd probably put Coq and Agda ahead of Idris in terms of being well known and established, but Idris is certainly pretty cool in how it tries to target practical programming.

Yeah - renewables are quicker to bring online, and allow for faster iteration and innovation. If Australia currently had nuclear power plants I definitely wouldn't be in favour of shutting them down, but it seems a better bet to invest in the renewable energy.

> Business changes are usually changes in logic, not in types.

Types _are_ logical propositions. In languages like Coq they are more expressive, and it's easier to leverage them as a way to constrain your implementation. Of course it's just a model, and there can be bugs in the specification, so it's not a silver bullet.

Awesome work! I've not had the greatest experience with Opam in the past for the reasons you mention - after using Cargo for a long time, it was a bit of a shock! This could do wonders to improve things!

Some questions:

- Is there any issues with sharing the same config file with another package manager? Ie. `package.json`?

- On a similar vein, why JSON, and not a config format that supports comments, like TOML?

- Will it be able to do Coq projects as well? I've not had a great experience trying to use Opam with it, and had to resort to using submodules. D:

> I used to point out to people that functional programming can be imperative and nobody (I do mean nobody I spoke to about this) would believe me on this.

Interesting. Monadic Haskell can be quite imperative if you want it to be, as can SML or OCaml. Scheme and Lisp have imperative parts too.

> and it's built on Chromium

That's a negative to me - again, too much browser engine consolidation. :/

> I stand corrected, as monomorphization is optional for parametric polymorphism but mandatory for ad hoc polymorphism.

It's not mandatory for ad-hoc polymorphism. Haskell desugars ah-hoc polymorphism to dictionary passing (although it often does inlining to reduce the overhead of this).

Oh, I must be mistaken then. So pointers are guaranteed not to be null? Can I mark pointers as nullable, and be forced to explicitly check?

Although there are differing ways to define dependent types, and they come in different varieties (dependent functions, dependent pairs/structs, very dependent types, dependent intersections, inductive types), they are all founded on a foundation of type theory. I guess if you want me to clarify, it is 'dependent types based on a well understood foundation from type theory'.

---

Edit: seems like Zig does have optional types! That is a good thing! https://ziglang.org/documentation/master/#Optionals

I wouldn't say it's inexcusable, but I'm definitely trying to avoid any systems language that has implicit null, and allows for data races and de-referencing uninitialized memory from safe code. So that only really leaves ATS and Rust, and rules out Nim, D, Zig, Jai... (for me at least).

Zig certainly has some cool ideas - I definitely think that we should be making the phase distinction more flexible. I do wish however that its compile time function evaluation was built on a firmer foundation, ie. using dependent types.

> This approach, technically termed ad hoc polymorphism (i.e. polymorphism without type system support)

Note that Haskell and Rust (and other languages) have adhoc polymorphism _with_ type system support via type classes/traits. I would class this more as 'duck-typed templates'.

> or binary bloat.

This is an orthogonal issue, to do with whether instantiations of parameterized types/functions are monomorphised or not. I would say the big issue with templates is that they are slow and produce hard-to decipher compile-time stack traces, because they are not checked at the instantiation site.

You can use most WebExtensions from Chrome with Firefox: https://addons.mozilla.org/en-US/firefox/addon/chrome-store-...

Been really enjoying Firefox, especially after Quantum. More devs should support and use it, lest we be beholden to Chrome for the rest of time.

> They tapped Yehuda Katz early on for this.

After trying three or four times to build one on their own that is!

I don't know about Crystal's preformance problems specifically, but I would be surprised if macros would take up much compile time. I would have guessed it was more to do with the fiendishly tricky type inference problem that they set for themselves (ie. global inference + subtyping + union types + inheritance + overloaded methods).

Yeah, what I was referring to when I mentioned marketing and communication design in another thread. You don't have to make false claims, you just have to shape your wording and content in order to target the right people in a more reliable way.

Prince is pretty powerful when it comes to print-specific stuff. We care about pagination, making tables look good across page breaks, footnotes, great justification, table of contents, non-sRGB color space handling, crop marks, etc. Also having great accessibility annotations (often mandatory for government documents). These are things that web browsers are less concerned with - print-to-PDF is more of an afterthought, where as for us it's our main area of focus.

Oh yeah! Definitely agree with this!

Marketing and good communication design is important though, if you want to actually reach new users. If somebody can't get the gist of what you're about from a glance, they are far less likely to invest a year into giving it a solid try.

As Mike says in a sibling comment, we use it quite heavily for implementing our HTML-to-PDF browser engine, https://www.princexml.com

It's a pretty handy general purpose language, kind of a combination of Prolog and Haskell. It's much easier to maintain a long-lived project in Mercury than one in Prolog due to the static typing, and it also generates much more efficient code. That said, it doesn't have the greatest documentation, so you might have to reach out on IRC, or the mailing list if you run into some challenges with it.

I always found react-redux's connect function maddeningly hard to understand, because it does far too many things all in one function. The types just expose that complexity, and make it plainly obvious that it should be split apart.

The great thing about types is that the make you think more about keeping you APIs nice and clean on a semantic level, not just about if the syntax in your examples look pretty. I really hope more library authors use them early on so they avoid such mistakes in the future. There's only so much the Flow and TypeScript devs can do to make up for those existing problems.

Afaik (I'm no security expert), as soon as you pushed them to a public repo you should change them all regardless of force pushing, because there's no way to take it back. Folks do trawl github for passwords and secrets.

I dunno, I do prefer having type directed editing (eg. auto case splitting, and autocomplete), so full type inference is less of a holy grail to me.

Damas-Hindley-Milner inference is also hyper-optimised to a specific point on the design space, and does an excellent job there, but (to echo Conor McBride) I would love to see less conflation of the ideas of execution phase, parametericity, and implicitness going forward.

That's why you go with bidirectional type checking instead. This scales much better to more interesting language constructs like rank-n polymorphism, and dependent types, gives better localised error messages, and the downside of having to have some top level annotations is worth it, because that's best practice anyway.