Why do people design dynamically typed (DL) languages over statically
typed languages (Sl)?

In the case of Lisp, it seems obvious, metaprogramming. That said, you
can metaprogram in SLs, so maybe it is not so obvious.

Note: When I talk of static type systems, I mean things like
Hindley-Milner with multi-parameter typeclasses and fundeps, and
certainly with type inference.  I do not mean the Java typesystem with
full type declarations for every variable and method.

Do generalise my remarks to interpreted languages, semi-static
typesystems, types as an optimisation, segfault-on-type-error (ouch),
etc, where applicable.  The languages discussed are extremes.  Almost
all languages fall in-between, using annotations or escape-hatches.
(Machine code is *very* dynamically typed: you can (try to) multiply a
string by a date then execute it.  <Name Omitted> is *very* statically
typed: people have spent hours writing code to prove that appending a
list of length X to a list of length Y produces a list of length X+Y.)

"You" means the programmer.  "Effort" includes time and money taken to
write the code, debug it, maintain it, etc.  A generic function can
contain many "methods", and which is run depends on the types of the
inputs/outputs of the generic function.

-----

A static typesystem does two things:
   {1} It allows the compiler to prove that your data-manipulations are
typesafe.
   {2} It lets the requirements of those proofs determine which code is
actually run (e.g. method dispatch on required return type).

To do these, it requires you to annotate your program to give enough
intermediate steps of those proofs that the compiler can figure the rest
out (datatype declarations, and maybe type declarations, along with type
inference).

If your proofs do not work, then that compiler will give you a type
error immediately, rather than you having to run the program with an
input that is a counterexample to your flawed proof.  Also, the proofs
are *absolute* proofs of whatever they claim to prove, whereas
(theoretically) any set of test-cases might have something missing.

OTOH, the compiler will want you to always have

These proofs are good for the humans who read your program.  If you see
a function parameter called "splitBefore" and it is an integer, you can
guess it is the index at which to split a list.  If it is a regex, then
you can guess the split will be before the point where the regex
matches.  Etc.  If you can immediately see that an parameter to a
function is a list in integers, then you will not need to study the
function and figure it out.  In fact, these annotations are so handy for
readers that SICP for Scheme tells you to put them in the function
comments even though the compiler can't see them there (Scheme is
dynamically typed).

-----

A dynamic typesystem does not require you to add the aforementioned bits
of proofs:
   {1} It allows you to write *any* program that will be type-safe while
it is running.
   {2} It lets the type that things have when the program is running
determine what code is actually run (is-number?, is-char?, is-string?,
or whatever the language calls them)

To do this, you keep all the proofs that things are typesafe in your
head (or in comments, etc).  You can understand type-safeness proofs
more easily than understanding them *and* explaining them to a compiler;
the compiler may not even be able to understand the proof, or it may
just be tedious and complex.

OTOH, If you get it wrong, some form of Bad Thing will happen (maybe
just an exception).  It will happen at run-time not compile-time, which
makes your debugging loop longer.

Usually, the compiler generates a program that checks at runtime that
conditions are satisfied for the program to keep going (run-time
type-checks).  This means that the running program must keep checking
some things that will be always true, because the compiler can't *prove*
they are always true.  It also means that things that haven't been
decided yet in the *running* program cannot influence it; e.g. you
cannot dispatch methods based on their required return type.

-----

One final thing I remember: an IDE for a dynamically-typed language can
give you a lot less help than one for a statically-typed language.  You
type "Foo.", and it just shrugs, because it has no idea what methods or
fields Foo might have.

Summary:
--------
Dynamic versus static typing is all about how much you tell the compiler
about your program, and how much it can do for you in return.  You can
tell the compiler what things should always be true, and it can prove
for you that they are always true, and deduce things that determine the
behaviour of your program.  But it takes effort to explain these things,
you won't often get them wrong, and you can usually just look at the
behaviour-determining things at run-time.

(While writing this, I have begun to really feel what theoretical people
have been telling me about for years: the relationship between programs
and proofs.  A program (or at least, a function) proves the existence of
something by constructing it, and static type-checking shows that the
construction technique is "valid".)