4 ms·
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
by stevan 11y ago
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 ∷ []
- murbard2 11y agoIt'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 11y agoIt'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.)
- danghica 11y agoI am aware of this -- I teach Agda :) But I think Agda is not quite as accessible as Python, that's what I meant. Cheers!
- ngrilly 11y agoHow 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".
- Dewie3 11y agoHe 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 11y agoYou would still need to program in Agda though :) Cheers!
- TheCoelacanth 11y agoOnly 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.