Live data from Hacker News

Dependent Haskell

serokell.io

11–20 of 92 posts

Re: Dependent Haskell

#11

This read like a troll piece. Every line rubbed me in some wrong way until I couldn't take it any more. > Haskell, at its core, is simple: it is just a polymorphic lambda calculus with lazy evaluation plus algebraic data types and type classes. This happens to be just the right combination of features to allow us to write clean, maintainable code that also runs fast. This is an explainabrag which is also wrong: langu…

Swift uses reference counting which is generally considered a form of garbage collection.

I agree, I felt like the author just wanted to talk about how great Haskell is. It made me think of the "smug lisp weenie" archetype.

Re: Dependent Haskell

#12

Does anybody care to explain dependent types? I’ve heard the term used in FP conversations but not sure I get it.

Most typed languages have two separate levels: expressions (and statements in imperative languages) and types. Dependent types unify those two levels into one. This allows one to use values in types, or vice versa, effectively making types first class in the sense that functional programming makes functions first class.

As an example this is Haskell's core language:

  data Expr b
    = Var   Id
    | Lit   Literal
    | App   (Expr b) (Arg b)
    | Lam   b (Expr b)
    | Let   (Bind b) (Expr b)
    | Case  (Expr b) b Type [Alt b]
    | Tick  (Tickish Id) (Expr b)
    | Type  Type
    | Cast  (Expr b) Coercion
    | Coercion Coercion

  data Type
    = TyVarTy   Var
    | LitTy     TyLit
    | AppTy     Type Type
    | ForAllTy  !TyCoVarBinder Type
    | FunTy     Type Type
    | TyConApp  TyCon [KindOrType]
    | CastTy    Type KindCoercion
    | CoercionTy Coercion
If you look closely you'll notice quite a lot of duplication between the two (see the first 4 and the last 2 constructors). Haskell is effectevily using the same language (lambda calculus) to describe types and expressions though with different syntax.

And this is Lean core language (a dependently type language):

  inductive expr
  | var         : nat → expr
  | sort        : level → expr
  | const       : name → list level → expr
  | mvar        : name → name → expr → expr
  | local_const : name → name → binder_info → expr → expr
  | app         : expr → expr → expr
  | lam         : name → binder_info → expr → expr → expr
  | pi          : name → binder_info → expr → expr → expr
  | elet        : name → expr → expr → expr → expr
  | macro       : macro_def → list expr → expr
Imo dependent types provide a surprising answer to the question "What is the best type system?". Different languages have different type systems and as they evolve to become more expressive at a certain point they become Turing complete (e.g. C++, Typescript, Haskell, ..). So we end up with two separate languages - the language itself to describe programs and the type system to describe types.

So what's the best type system? Dependent types' answer: the language itself. Instead of having two separate languages, have a single language that acts as its own type system, powerful enough to describe both programs and types. Then types become first class - you can pass them to a function as parameters, or return them as values, or use any function at compile time.

In physics progress usually comes in the form of unification. Two seemingly separate phenomena (say electricity and magnetism) turn out to be described by a single theory. Dependent types provide such a unification between expressions and types in programming languages. Imo definitely a step forward in the noisy sea of programming languages.

That's not even touching the mathematical side of things, Curry-Howard correspondence, proof assistants and using dependent types for proving theorems.

Re: Dependent Haskell

#13
post #3

I really do think Haskell is a wonderful tool, but: "Haskell, at its core, is simple: it is just a polymorphic lambda calculus with lazy evaluation plus algebraic data types and type classes." In a different context, I would have interpreted that as a sarcastic parody of Haskell evangelists. Really, I feel like everyone who is going to read that article will either already know that, or will have no idea what that se…

Well, both System Fc and Haskell Core are quite simple and consistent. It's much more concise than any imperative language with dozens of corner cases, yet quite powerful.

Re: Dependent Haskell

#14
post #3

I really do think Haskell is a wonderful tool, but: "Haskell, at its core, is simple: it is just a polymorphic lambda calculus with lazy evaluation plus algebraic data types and type classes." In a different context, I would have interpreted that as a sarcastic parody of Haskell evangelists. Really, I feel like everyone who is going to read that article will either already know that, or will have no idea what that se…

What that quote means is that you can take a Haskell program and compile it into lambda calculus and this is what GHC is more or less doing.

This has important implications. From a theoretical perspective, it's easier to prove that the language remains sound when you add new features. But also from a more practical point of view, it's easier to work on compiler backends for a more minimal language, to target new CPUs or for applying optimizations.

These issues are very well known to language designers. E.g. one of the big changes in Scala 3 / Dotty is that it's supposedly based on "DOT Calculus". Having the ability to "desugar" the language into a simpler language that is provably type safe is pretty awesome.

What makes Haskell interesting is that the developers using Haskell also become acquainted with such issues. Haskell is a language and ecosystem that raises the knowledge ceiling for its users. And there aren't many languages around that do that ;-)

Re: Dependent Haskell

#15

Does anybody care to explain dependent types? I’ve heard the term used in FP conversations but not sure I get it.

When the type of a function mentions its parameter, it’s a dependent type (just like a normal function that mentions it’s parameter is a “dependent value”, so to speak.

Usually though one speaks of dependent types only when the parameter can range over not just types.

Re: Dependent Haskell

#16
post #7

Does anybody care to explain dependent types? I’ve heard the term used in FP conversations but not sure I get it.

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 th…

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.

Re: Dependent Haskell

#17

Does anybody care to explain dependent types? I’ve heard the term used in FP conversations but not sure I get it.

Imagine that you take a type from C or Java or something and add the ability to convert it into another type. I'm not talking about casting an int to a float, but actually manipulating the type without doing anything on the data side.

Now allow arbitrary programs to be types. We'll call these type programs.

Now imagine a game where you take one type program and try to convert it into another while proving to the compiler that it still does the same thing.

For example, say you had a function foo (int x) { return x+1; }, and the type program A “foo(a+1)”, and the type program B “foo(foo(a))”. Your job would be to change A to look exactly like B, or vice versa, using commands built into the language itself.

Why would you want to do this? Because it's been shown using a certain type of mathematics, called constructive mathematics, you can create type programs to represent any hypothesis you would like: m + n = n + m, for example. Then you can use the built in commands to change a type into another type to represent a proof of the hypothesis.

In this way you can prove hypotheses related to your program, (or anything really) as long as you construct the right types and use the built in commands to change prove the hypotheses true.

You really need to learn a lot of things to understand how this translation from types to proofs work, so I didn't try to explain that here.

I find the whole thing fascinating myself, but haven't gone too deeply into it.

(BTW, if anyone more knowledgeable sees something I've written that is wrong here, please correct me, for my own information more than anything else)

Re: Dependent Haskell

#18

This read like a troll piece. Every line rubbed me in some wrong way until I couldn't take it any more. > Haskell, at its core, is simple: it is just a polymorphic lambda calculus with lazy evaluation plus algebraic data types and type classes. This happens to be just the right combination of features to allow us to write clean, maintainable code that also runs fast. This is an explainabrag which is also wrong: langu…

I love haskell, but agree that the article is corny as hell (sorry, author!). Having the text read by multiple people before publishing could have made this a lot better (and still can).

Dependent types on the other hand are great! Looking forward, good luck!

Re: Dependent Haskell

#19
post #11

This read like a troll piece. Every line rubbed me in some wrong way until I couldn't take it any more. > Haskell, at its core, is simple: it is just a polymorphic lambda calculus with lazy evaluation plus algebraic data types and type classes. This happens to be just the right combination of features to allow us to write clean, maintainable code that also runs fast. This is an explainabrag which is also wrong: langu…

Swift uses reference counting which is generally considered a form of garbage collection. I agree, I felt like the author just wanted to talk about how great Haskell is. It made me think of the "smug lisp weenie" archetype.

It does reference counting, but it's not mark-and-sweep stop the world reference counting. It's as garbage collected as shared_ptr and doesn't try to collect cycles. Feels a bit weird to put that under the same bucket as Java.

Re: Dependent Haskell

#20

This read like a troll piece. Every line rubbed me in some wrong way until I couldn't take it any more. > Haskell, at its core, is simple: it is just a polymorphic lambda calculus with lazy evaluation plus algebraic data types and type classes. This happens to be just the right combination of features to allow us to write clean, maintainable code that also runs fast. This is an explainabrag which is also wrong: langu…

That "explainabrag" pissed me off too. I feel like that kind of thing is super typical among Haskell bloggers.
Post reply on HN