Create simple functions with dependent types

Question

I am learning from the official documentation. I have tried to modify the first example:

isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat

mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []

Here are my tries:

compute_type : Integer  -> Type
compute_type 1 = Nat
compute_type 2 = String

--foo : (x : Integer) -> compute_type x
-- foo 1     = Z
-- foo 2 = ?one --unwords ["A", "B", "C"]

Error:

{-
first_class_type.idr:7:13:
  |
7 | foo 1     = Z
  |             ^
When checking right hand side of foo with expected type
        compute_type 1

Type mismatch between
        Nat (Type of 0)
and
        compute_type 1 (Expected type)
-}

ct2 : String -> Type
ct2 "Integer" = Integer
ct2 "String"  = String
foo2 : (s : String) -> ct2 s
-- foo2 "Integer" = 42

Error:

{-
   |
28 | foo2 "Integer" = 42
   |                  ~~
When checking right hand side of foo2 with expected type
        ct2 "Integer"

ct2 "Integer" is not a numeric type
-}

ct3: Bool -> Bool -> Type
ct3 True True = Nat
ct3 False False = String

foo3: (a: Bool) -> (b: Bool) -> (ct3 a b)
-- foo3 True True = Z
-- foo3 False False = "Stringggg"

Error:

{-
first_class_type.idr:44:18:
   |
44 | foo3 True True = Z
   |                  ^
When checking right hand side of foo3 with expected typ
        ct3 True True

Type mismatch between
        Nat (Type of 0)
and
        ct3 True True (Expected type)

Holes: Main.foo3, Main.foo2
-}

ct4: (b: String) -> Type
ct4 "Integer" = Integer
ct4 "String"  = String
foo4: (s: String) -> ct4 s -> Integer
-- foo4 "Integer" x = x
-- foo4 "String" ss = 987

Error:

{-
   |
67 | foo4 "Integer" x = x
   |                    ^
When checking right hand side of foo4 with expected type
        Integer

Type mismatch between
        ct4 "Integer" (Type of x)
and
        Integer (Expected type)
-}

I have no idea why my functions do not returns types. They look similar to Idris codes but they do not work.

Answer 1

Your type functions are not total. You can check this with :total foo or specifying, that the function should be total:

%default total
-- or
total foo : Integer -> Type

Only total functions are get resolved in the type checker, otherwise it may or may not run forever. If you want to stick to Integer and String, to make your functions total, you can just add a default case:

compute_type : Integer  -> Type
compute_type 1 = Nat
compute_type _ = String

foo : compute_type 1
foo = Z