There’s also a version for very young children (K-2) - ScratchJr.
My friend who does CS education told me about Picobot which isn’t a language, but rather a way to teach state machines. It’s pretty much the most fun thing ever even for someone like me who is probably at least an intermediate level in Automata and who basic state machines should be interminably boring to. She reports that the students she teaches have been caught playing with it in their free time.
Suggesting possible data representations to the compiler is only one reason why we have types. Types also document code, they help to structure it, they help to enforce abstraction, they express invariants, they’re a basic sanity check, they help external tools like IDEs understand your code, and so on. If your type language is expressive enough, you can guess what functions do pretty reliably just by looking at the type. I know, in Haskell, for instance, that the only possible total function of type
a -> a
is the identity function, for instance. In Agda, where the type language is more expressive than in Haskell, my types don’t just hint at what a function does, they can completely describe its behaviour:
module Scratch where
open import Data.Nat
open import Relation.Binary.PropositionalEquality
data List (α : Set) : Set where
[] : List α
_∷_ : α → List α → List α
map : {α β : Set} → (α → β) → List α → List β
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs
length : {α : Set} → List α → ℕ
length [] = zero
length (x ∷ xs) = suc (length xs)
map-id : {α : Set} → (xs : List α) → map (λ x → x) xs ≡ xs
map-id [] = refl
map-id (x ∷ xs) = cong (_∷_ x) (map-id xs)
map-length : {α β : Set} → (f : α → β) → (xs : List α) → length (map f xs) ≡ length xs
map-length f [] = refl
map-length f (x ∷ xs) = cong suc (map-length f xs)
etc.
Man, I have to try functional languages again. That was really hard to read, but I feel like it would be really beneficial to interpret that syntax/model of thinking fluently for certain applications.
I used to be decent in Haskell too… (but fuck OCaml, it has the smartdumbest compiler I’ve ever seen. Like, it can tell when you haven’t covered all possible cases in your logic, but it has exactly one syntax error called “syntax error”)
Edit: Though I have to ask, are all the Greek letters part of the Agda syntax? It seems like that would be rather obnoxious since they’re not part of most US keyboards.
The best language to learn first is APL, of course. Or perhaps SNOBOL.
OK, seriously: it depends on what the end goal is. But for someone who wants to be a serious programmer, doing software engineering rather than just writing little scripts to automate a few tasks, I’d suggest Java.
I admit it sets a fairly high hurdle for getting started, a point against it (especially compared to scripting languages). On the other hand, learning any of the Java packages like those for database, security, networking, etc., is a great way to learn the underlying subjects, since they codify the classical solutions. Meanwhile, it’s object oriented so you get off on the right foot in that regard.
I’d like to recommend Python as a great first scripting language, but can’t simply due to the way it’s documented. It’s documented in a way that makes sense to a computer scientist in the languages area, rather than for someone who just wants to learn how to program (or even, just how to program in Python). Perl (a language I tend to loathe, usually due to trying to read perl scripts written by others) is way better in this regard, but I doubt I’d recommend it either.
I loved that book, but most of the objections are pedantic, and aren’t really issues for new learners. I don’t recommend Pascal as a system implementation language or for serious software engineering, but back in the day, it was a good one for a first language.
I found Modula III interesting, but I felt that they went too far to make the BNF description of the language terse, at the expense of brevity and clarity in programs written in the language. When trying it out, I kept wondering why I had to do apparently clumsy things. After consulting the one-page grammar, I saw: it allowed keeping some definition a one-liner rather than a multi-part production. I didn’t ever use it in any serious work, though. Since it didn’t catch on, it’d be a bad choice even if it was a great language.
Talking about Agda’s syntax is a bit complicated because:
[ul]
[li]There’s very little builtin to the language itself. For example, the Booleans are defined within the language:[/li]
data Boolean : Set where
true : Boolean
false : Boolean
Further, things that you would normally expect to be primitive in other languages, such as if-then-else, are normal functions in Agda. For example:
if_then_else_ : {a : Set} -> Boolean -> a -> a -> a
if true then t else f = t
if false then t else f = f
Similarly with things like tuples, lists, sets, finite maps, and so on. Even propositional equality is defined within the language:
data _≡_ {α : Set} (a : α) : α → Set where
refl : a ≡ a
In Agda, you get a dependent function space, and the ability to define new inductive (and co-inductive) types. Everything else is defined within the type theory.
[li] Agda accepts Unicode but it also understands ASCII alternatives for the few keywords that are builtin to the language, like the function space arrow ->.[/li][li] Agda allows you to define mixfix syntax freely. Any identifier with underscores in it will be parsed and pretty-printed in a mixfix style. See if_then_else_ above.[/li][li] The Agda module system allows you to rename any constant that you don’t like freely when importing that module. If module Data.Nat exports the type ℕ (which it does), and I don’t feel like using that name in my module, then at the top of my module I’d write: open import Data.Nat renaming (ℕ to Nat), and then use Nat henceforth.[/li][li] Unicode input isn’t that big a deal as the emacs mode for Agda handles it all. It automatically replaces \bn with ℕ for instance, when you type it in.[/li][/ul]