[stevan]

I'd disagree with the two statements:

> People who think they understand something about the theory of programming languages, including me, tend to agree that what Python does is wrong.

> In fact you can program heterogeneous lists in dependently typed languages, but it’s unreasonably complicated.

Here's some Agda code that shows that both heterogeneous if statements and lists make sense and are easy to work with in type theory.

    data Bool : Set where
      true false : Bool

    if : ∀ {ℓ} {P : Bool → Set ℓ} (b : Bool) → P true → P false → P b
    if true  t f = t
    if false t f = f

    postulate Char : Set
    {-# BUILTIN CHAR Char #-}

    data ℕ : Set where
      zero : ℕ
      suc  : ℕ → ℕ

    {-# BUILTIN NATURAL ℕ #-}

    ex₁ : ℕ
    ex₁ = if {P = λ b → if b ℕ Char} true 0 'a'

    infixr 5 _∷_

    data List {a} (A : Set a) : Set a where
      []  : List A
      _∷_ : A → List A → List A

    data HList : List Set → Set where
      []  : HList []
      _∷_ : ∀ {A As} → A → HList As → HList (A ∷ As)

    ex₂ : HList (ℕ ∷ Char ∷ (ℕ → ℕ) ∷ [])
    ex₂ = 1 ∷ 'a' ∷ suc ∷ []

[danghica]

I am aware of this -- I teach Agda :) But I think Agda is not quite as accessible as Python, that's what I meant. Cheers!

[murbard2]

It's great to have an example, but could you add inline comments for those of us who aren't familiar with Agda's syntax?

[Retra]

It's basically Haskell with unicode identifiers and mixed-fixity. (I.e., _::_ is an infix function of two arguments, and the _'s represent "holes" for the arguments.)

[ngrilly]

How can you compare that code with the Python one liner in the original article? It's interesting, of course, but it's not "easy to work with".

[TheCoelacanth]

Only the two lines starting with ex1 for heterogeneous if and the two lines starting with ex2 for heterogeneous lists are directly comparable to the Python examples. The rest is just defining what a boolean is, what a natural number is, what a character is, what if is, what a list is, what a heterogeneous list is, etc., to provide a full foundation for the examples.

[Dewie3]

He explicitly gives standard machinery like the a boolean type and natural numbers, presumably to show more clearly what the parts are built up from. You probably wouldn't need to write all of that to use HList at a later point.

[danghica]

You would still need to program in Agda though :) Cheers!