myType : Nat -> Type
myType Z = Int
myType (S x) = List (myType x)

create : (n:Nat) -> myType n
create Z = 0
create (S x) = [create x]

useValue : (n:Nat) -> myType n -> String
useValue Z v = show v
useValue (S x) v = concat $ map (useValue x) v

main : IO ()
main = do
  ns <- getLine
  let n = cast ns
  putStrLn $ useValue n (create n)

ВВ>Никакой это не немерлизм. Это, может, в OCaml не так, где не потрудились ХМ допилить. А в языках с полиморфными операторами ты даже функцию "sum x y =x+y" иначе не типизируешь. Ибо какой у нее тип?

Prelude> let sum x y = x + y
Prelude> :t sum
sum :: Num a => a -> a -> a

... -- myType и create как в оригинале
useValue : (n:Nat) -> myType n -> String
useValue Z v = show v
useValue (S x) v = "[" ++ (concat $  map (useValue x) v) ++ "]"

main : IO ()
main = do
  ns <- getLine
  let n = cast . cast $ ns
  putStrLn $ useValue n (create n)

C:\prog\idris>idris nlist.idr -o nlist.exe

C:\prog\idris>nlist
1
[0]

C:\prog\idris>nlist
0
0

C:\prog\idris>nlist
4
[[[[0]]]]

C:\prog\idris>nlist
42
[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[0]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

> let sum x y = x+y
let x = sum 2 3
let y = sum "one," "two";;

  let y = sum "one," "two";;
  ------------^^^^^^

stdin(3,13): error FS0001: В данном выражении требовалось наличие типа
    int    
, но получен тип
    string

> let sum x y = x+y
sum "One," "Two"
sum 1 2;;

  sum 1 2;;
  ----^

stdin(3,5): error FS0001: В данном выражении требовалось наличие типа
    string    
, но получен тип
    int

ВВ>>Или я не прав и круче зависимых типов только яйца?

DM>Да, вывод именно такой, конечно.

open espec

test1 =
  test "With list"
  given [1]
    when (++) [2]
    should be [1,2]
    when tail
    shouldn't be [1,2]
    should be [2]

test2 = 
  test "With int"
  given 4
    when (+) 5
    should be 9
    when negate
    should be -9
    when (+) 13
    should be 4

[] 
  |> addTest test1
  |> addTest test2
  |> run
  |> formatResult

Test session started.

Test "With list" (failed 0, errors 0):
  given [1]
    when (++) [2] -> [1,2]
    should be [1,2] -> success
    when tail -> [2]
    shouldn't be [1,2] -> success
    should be [2] -> success

Test "With int" (failed 0, errors 0):
  given 4
    when (+) 5 -> 9
    should be 9 -> success
    when negate -> -9
    should be -9 -> success
    when (+) 13 -> 4
    should be 4 -> success

Total tests:2 Failed: 0

DM>Как видим, о рантайм значениях можно рассуждать статически. Сюрприз!

  type Range_Type is range -5 .. 10;

module Test (foo) where
foo x = x

VE>module Test (foo) where
VE>foo x = x
VE>

> let sum x y =x+y;;

val sum : x:int -> y:int -> int

ВВ>Это помогло или сейчас будет очередная истерика в стиле самодовольного невежества?

Ну да, легко. Отложенная типизация в действии =)

Prelude> sum = \a b -> a + b
sum :: Integer -> Integer -> Integer
Prelude> sum a b = a + b
sum :: Num a => a -> a -> a
Prelude> let sum = \a b -> a + b in sum 2.0 40
42.0
it :: Double

> let inline sum x y = x+y;;

val inline sum :
  x: ^a -> y: ^b ->  ^c
    when ( ^a or  ^b) : (static member ( + ) :  ^a *  ^b ->  ^c)

> let x = sum 2 3;;

val x : int = 5

> let y = sum "one," "two";;

val y : string = "one,two"

> let sum x y = x+y;;

val sum : x:int -> y:int -> int