Как-то странно, что на РСДН ещё не появилась ссылка о сабже. Там приводится очень интересная работа Тёрнера, раскрывающая тему терминируемости алгоритмов, приводится базовый язык, в котором чётко разделяется data как базис примитивных типов и codata как базис для структурной рекурсии. По сути он говорит, что даже haskell недостаточно строг (формален), т.к. допускает _|_ (bottom), однако эта нестрогость даёт достаточную свободу для решения практических задач, поэтому традиционное ФП он называет слабым, а искомую систему — сильным ФП (аналогично языкам со слабой и сильной системами типов).