JavaScript надежность

предполагалась полиморфная реализация, потому что потом что-нибудь типа (map (+ 1) (flatten '(1 (2 (5) 5) (3 4 5))) уже не чекнется (и возвращаемся к началу - корректный терм, не чекается :)).

flatten x = case fromDynamic x of
  -- pair
  Just [] -> []
  Just (l:r) -> flatten l ++ flatten (toDyn r)
  -- не pair
  Nothing -> [x]

В Scala PM по типо-термам и автоматическое поднятие позволяет сделать немного нагляднее, без цепочек из fromDynamic и toDyn. Но это же чисто технически момент.

Тип идет как раз с not-типами, о которых я уже говорил (то есть компилятор должен знать что в третей строке НЕ пара).

Это какой-то хардкор. В динамике просто рантайм разбор (как в if/switch по тегу) - если детектировали пару делаем одно, если нет - другое. В типах это никак не отражается, там просто T. А то так можно в типы переносить какие угодно утверждения и требовать передачу вместе с данными доказательств свидетельствующих об этих утверждениях - о том что данные принадлежат таким-то диапазонам, связаны такими-то отношениями, удовлетворяют таким-то предикатам. Например, fromMaybe нельзя написать, но если добавить свидетелей для данных:

fromMaybe : {A : Set} → (x : Maybe A) → ∀ {some} {is-just : x ≡ just some} → A
fromMaybe (just x) = x
fromMaybe nothing {is-just = ()}

test₁ : ⊤
test₁ = fromMaybe (just tt) {is-just = refl}

test₂ : ⊤
test₂ = fromMaybe nothing {is-just = {!!}} -- nothing ≡ just tt

Или требовать в типах доказывать, что flatten не удаляет и не добавляет каких-то элементов.

что-нибудь типа (map (+ 1) (flatten '(1 (2 (5) 5) (3 4 5)))

def addOptional(x: Any, y: Any): Option[Int] = (x, y) match {
  case (xi: Int, yi: Int) => Some(xi + yi)
  case _ => None
}

def addExceptional(x: Any, y: Any): Int = (x, y) match {
  case (xi: Int, yi: Int) => xi + yi
  case _ => throw new IllegalArgumentException("bad addition: " + x + " + " + y)
}

scala> flatten(List(1, List(Some('2'), null), "3", 4, "5", 6)) map (x => addOptional(x, 1))
res0: List[Option[Int]] = List(Some(2), None, None, None, Some(5), None, Some(7))

scala> flatten(List(1, List(Some('2'), null), "3", 4, "5", 6)) map (x => addExceptional(x, 1))
java.lang.IllegalArgumentException: bad addition: Some(2) + 1

fromDynamic x

Нет-нет, это другой терм.

Это какой-то хардкор. В динамике просто рантайм разбор (как в if/switch по тегу) - если детектировали пару делаем одно, если нет - другое.

Чтобы эмулировать поведение динамики, нужны not-типы, т.к. ф-я должна быть полиморфной а в полиморфном аргументе должно фиксироваться до каких пор делать flatten.

В типах это никак не отражается, там просто T.

И как мне потом к этому «просто T» применить ф-ю, которая не определена на Any?

А то так можно в типы переносить какие угодно утверждения

Ну зависимые типы - оно и есть.

Это уже другие термы, нам нужные родные + и так далее.

И как мне потом к этому «просто T» применить ф-ю, которая не определена на Any?

Лисповый T это и есть скальный Any. В динамике у нас нет функций которые не определены на Any, так что если нужно переводить лисповые '+ и т.п., которые T ... -> T, то нужно брать соответствующие Any ... -> Any, а не «родные», которые хоть и выглядят так же («+» и т.п.) на самом деле совсем _другие_ функции (и даже не функции, а методы).

Так что:

scala> ((x: Int) => x + 1).asInstanceOf[(Any) => Any]
res1: Any => Any = <function1>

scala> flatten(List(1, List(2, 3), 4, 6)) map ((x: Int) => x + 1).asInstanceOf[(Any) => Any]
res2: List[Any] = List(2, 3, 4, 5, 7)

scala> flatten(List(1, List(2, "3"), 4, 6)) map ((x: Int) => x + 1).asInstanceOf[(Any) => Any]
java.lang.ClassCastException: java.lang.String cannot be cast to java.lang.Integer

Или сделать Ordering и Numeric/Integral traits на Any:

trait DummyOrdering[T] extends Ordering[T] {
  def compare(x: T, y: T) = 0
}

trait AnyIsIntegral extends Integral[Any] {
  type T
  val integral: Integral[T]
  def plus(x: Any, y: Any) = integral.plus(x.asInstanceOf[T], y.asInstanceOf[T])
  // ...
}

implicit object AnyIntIsIntegral extends AnyIsIntegral with DummyOrdering[Any] {
  type T = Int
  val integral = implicitly[Integral[T]]
}

def test() = {

  val anyIntegral = implicitly[Integral[Any]]
  import anyIntegral._

  val mono = List(1, List(2, 3), 4, 5)
  val poly = true :: mono

  println("flatten and map on `mono': " + (flatten(mono) map (x => x + 1)))

  try {
    println("flatten and map on `poly': " + (flatten(poly) map (x => x + 1)))
  } catch {
    case reason => println("can't map on: " + flatten(poly) + " (" + reason + ")")
  }
}

scala> test()
flatten and map on `mono': List(2, 3, 4, 5, 6)
can't map on: List(true, 1, 2, 3, 4, 5) (java.lang.ClassCastException)

asInstanceOf

Это как раз [может быть] небезопасное опускание типа, Scala его, естественно, автоматически делать не будет. Методы + и т.п. для Any из trait AnyIsIntegral extends Integral[Any], таким образом, небезопасные by design, прямо как в лиспе.

О, в скале даункасты есть? Так значит скала - динамически типизированный язык. Естественно, на ней можно написать все что можно написать в динамике - вопрос снят :)

Но типизированного flatten мы в данном случае и не видим - мы видим нетипизированный flatten :)