CODEWITHSUNDEEP
idris
Stefan Dorn
Stefan Dorn

Reputation: 599

Problem with dependent types function in Idris

I have just started reading a book "Type-driven development" and tried my simple example with dependent types. It should return a string for negative numbers and Integer for the positive ones. I started with 2 holes:

StringOrInt : Bool -> Type
StringOrInt b =
  case b of
    True => Integer
    False => String

getStringOrInt : (x : Integer) -> StringOrInt (x > 0)
getStringOrInt x =
  case x > 0 of
    True => ?x
    False => ?s

If I take a look at holes definition it looks very complicated and not helpful at all:

x : case with block in Prelude.Interfaces.Prelude.Interfaces.Integer implementation of Prelude.Interfaces.Ord, method > (ifThenElse (intToBool (prim__eqBigInt x 0))
                (Delay EQ)
                (Delay (ifThenElse (intToBool (prim__sltBigInt x
                                                               0))
                                   (Delay LT)
                                   (Delay GT))))
    x
    0 of
      True => Integer
      False => String

So how to write this function?

Upvotes: 1

Views: 197

Answers (1)

Stefan Holdermans
Stefan Holdermans

Reputation: 8050

Use with rather than case to leverage dependent pattern matching and have the type checker substitute the appropriate Boolean for x > 0 in the result type for each alternative:

StringOrInt : Bool -> Type
StringOrInt True  = Integer
StringOrInt False = String

getStringOrInt : (x : Integer) -> StringOrInt (x > 0)
getStringOrInt x with (x > 0)
  getStringOrInt x | True  = x
  getStringOrInt x | False = "<= 0"

Upvotes: 2

Related Questions