HN Theater @HNTheaterMonth

I don't know, some of that is at least starting to happen with Idris 2, though not in the exact way predicted: https://www.youtube.com/watch?v=mOtKD7ml0NU (Type Driven Development with Idris 2)

Short summary of linked video: when your type system is powerful enough you can restrict the set of possible implementations to the point that the compiler can make a decent guess as to what the program should be to satisfy the type signature.

You don't need the tests. You need only the types.

And especially you don't need "artificial dumbness", which does not understand code, and therefore won't produce correct results, but just an advanced programming language. Say hello to Idris! :-)

https://www.youtube.com/watch?v=mOtKD7ml0NU

⬐ chriswarbo

If you're completely specifying the behaviour then you're writing a program "manually"; that's what programming is.

Using a dependent type system to specify that behaviour is essentially a form of declarative/logic programming, similar to Prolog.

Deriving an implementation of those types automatically (e.g. by having the elaborator perform a proof search) is equivalent to compiling your pseudo-Prolog ahead-of-time.

It's certainly interesting that such a "compiler" can be guided (e.g. via elaborator reflection), but that's more useful for optimisation rather than implementation. (Note that in some cases, such 'optimisation' might be required for the proof search to finish before the heat death of the universe!)

SAT solvers are starting to be used as tooling for functional languages - Liquid Haskell uses one for refinement types[1], and Djinn uses one for suggesting functions given a type[2]. Similarly to Djinn, Edwin Brady gave a presentation on using an SMT solver to do live code suggestions/implementation inference in the successor to Idris[3].

[1] https://ucsd-progsys.github.io/liquidhaskell-blog/

[2] http://lambda-the-ultimate.org/node/1178

[3] https://www.youtube.com/watch?v=mOtKD7ml0NU

Until yesterday it was officially called "Blodwen" a "prototype successor to Idris", so I assume the fact that it's now officially being called a "pre-alpha implementation of Idris 2" means it's somewhat closer to being ready, but is there some specific announcement about the exact significance of it being officially called Idris 2 now?

Edit: Never mind, I found the official announcement on the Idris mailing list: https://groups.google.com/forum/#!topic/idris-lang/PQSozmTvt...

He says "No doubt I'll say more about this over the next few weeks," so it sounds like he's planning on making a more detailed announcement later.

Edit 2: Also, as someone who hasn't been following Blodwen or how it's different from Idris 1, this looks like a good introduction: https://www.youtube.com/watch?v=mOtKD7ml0NU

Idris lang seems awesome with the atom plugin. :)

Did not use it yet but I hope it will get more attention.

https://youtu.be/mOtKD7ml0NU

Hoogle is pretty nice, and few other languages had an equivalent until quite recently.

I'm hopeful that cool type-powered IDE features will start to arrive once haskell-ide-engine is a bit more stable. It's getting there!

There are some pretty awesome IDE ideas in Haskell-ish languages like Idris [1], too. There is some movement towards dependent types in Haskell, so it might get similar features one day.

[1] https://www.youtube.com/watch?v=mOtKD7ml0NU

Idris does this with a REPL-like interface:

https://www.youtube.com/watch?v=mOtKD7ml0NU

> In the general-purpose programming context, imagine if you could give examples of a program output (domain data) along with a skeleton of a program (source file with incomplete parts) and ask a system to fill in the holes.

This part reminds me of some of capabilities of the Idris compiler [1]. In an Idris program you can leave "holes" to stand in for incomplete parts of a program [2], and the compiler can infer various bits of code from types and holes. In a demo of the in-progress Idris 2 compiler [3], Edwin Brady refers to it as a "lab assistant" and shows it writing a whole function when given a function type.

[1] http://docs.idris-lang.org/en/latest/tutorial/interactive.ht...

[2] http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html...

[3] https://www.youtube.com/watch?v=mOtKD7ml0NU

I agree about its availability.

I think it's far more useful than you seem to, though. Reducing the problem space is huge. It's why macro programming (ala Lisp) is so dangerous. It's why I left Haskell for Python, and why I often wish I was using Idris[1], which pretty much reads your mind and writes what you meant. It's true of coding generally, but SQL programming especially, that there's a conceptually obvious, small space of reasonable programs, but because we're writing in text, we're free to roam over an enormous superspace of (occasionally) wrong or (usually) meaningless programs.

[1] https://www.youtube.com/watch?v=mOtKD7ml0NU

⬐ nubslayer

I don't really have an OSX computer to use it on, so it's not that useful to me. I could probably make the same or better in a few hours.

Not sure exactly what you mean by wrong or meaningless programs. (edit3) I'm not sure it's possible to write a meaningless SQL statement.

Edit: it seems like the authors don't see it as that useful. I think the page said they are still looking for use-cases, or something. Have you contacted them?

Edit2 (fta): "However, as of Jan 2019 we’re tabling the project until we have a concrete, motivating use case to inform further development."

Dependent types are types which depend on values. As an example, think of the cons procedure: (List A, A) -> List A. It takes a List of A's and an A and returns a List of A's. With dependent types you can write this as (List n A, A) -> List n+1 A. This tells us that cons takes a List of A's with length n and an A returns a List of A's with length n+1.

Edwin Brady shows off some examples in Idris here[1]. I thought the matrix example was really impressive.

[1] https://www.youtube.com/watch?v=mOtKD7ml0NU

⬐ joe_the_user

When I see this definition, I scratch my head and wonder why this isn't a different way to introduce object orientation, generics, c++ parameterized templates and such.

⬐ None

None

⬐ RossBencina

Yes. C++ templates provide some subset of what you can do with dependent types in Idris.

⬐ logicchains

The key difference with C++ templates is that in C++ you can't have a type parameterised by a value that's only know at runtime, e.g. a std::array<N> where N is read from stdin. In a dependently typed language, you can. Object orientation is a different matter entirely; in the sense it implies Java-style class-based inheritance, it's almost in the opposite spirit to dependent types, as such late-binding (virtual methods) means it's possible to call methods such that the compiler has no idea which method will be called at compile time, making it hard to reason about the code at compile time.

⬐ None

None

⬐ tpush

I'm really a fan of the type-driven development process Edwin shows of here.

Especially the part where it can generate the correct matrix transposition logic as soon as it's been told that 'matrix' can only be used once. Very impressive.

I really hope at least some of that catches the interest of mainstream language designers/communities.