4 ms·

I have think in something like this, but far simpler: Why the (avg) languages can't define types like in a database language? (ej: Age:Int, Check: x > 0 & x < 2

• chriswarbo 12y ago
  > However, with this: I get how can be usefull for data directly in the code, but how this work with data that come from somwhere? If i feed a CSV with numbers, what happend when some is 0? The same thing that happens in any language; have a validation layer which checks whether the incoming data is zero or not. If it is, then do something appropriate (eg. print an error and halt), if not then you can safely pass if to your non-zero function. See http://existentialtype.wordpress.com/2011/03/15/boolean-blindness/ http://existentialtype.wordpress.com/2011/03/15/boolean-blin...
• jonsterling 12y ago
  So the way it works when your data comes from somewhere and you don't know if it is "clean" is that you write a decision procedure to "find out". So the simplest use case is you've got a type like `{x : String | x.length < 10}`: that is, the type of strings which have length less than ten. A value of that type is going to be a pair `<str, proof>` where `proof` is an object which witnesses the fact that `str` has a length less than ten. Now, it is a decidable property whether or not a string is shorter than 10 chars long. You can easily construct a function with the following type: decideValidity : (str : string) -> Either (str.length < 10) (Not (str.length < 10)) This function is defined by induction on the string. Now you want to receive such a string from user input. Crucially, the logic of your program is going to operate on data that's already been validated: so your program will only deal with `{x:String | x.length < 10}`; we just need to shore up the boundaries between your program and user input. yourComputation :: {x:String | x.length < 10} -> Something main : IO () main = do userInput <- getLine case (decideValidity userInput) of Left prf -> do print (yourComputation <userInput, prf>) Right nope -> print "The input was invalid"
  • munro 12y ago
    Is it possible with Idris to programmatically create the `decideValidity` function? Conceptually it seems trivial to do, I could imagine building it with meta programming. My crazy pseudo code-- :D decideValidity : (p : Proof) -> a -> Either (p a) (Not (p a))
    • pavpanchekha 12y ago
      No—there are many properties that cannot be decided. For example, many programs can be proven to halt in finite time. For example, you can imagine a way to prove that the program return 0 always halts. However, testing for this property is impossible (Halting Problem). More generally, it is not possible to test a general predicate for satisfaction. Even things that are decidable in principle may not be decidable quickly (SAT). On the other hand, there is a lot of space for simple predicates like "str.length < 10" to be decided automatically, since the proofs for these can be constructed with only forward search.
      • munro 12y ago
        Wouldn't the proposed function then just not compile for the instances were it would be impossible to test, as desired? It would still be useful for where it does work, like in the code you provided. Seems like a lack of meta programming to me if it's not currently possible.
        • tel 12y ago
          You can sort of do this sometimes. Consider Idris' decidable equality module: https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Decidable/Equality.idr https://github.com/idris-lang/Idris-dev/blob/master/libs/pre... Idris has type classes and it produces a polymorphic total function `decEq` for any type which instantiates the class DecEq. decEq :: DecEq t => (x : t) -> y -> Dec (x = y) where Dec denotes a decidable type, something like (but not actually) data Dec t where Yes : t -> Dec t No : Not t -> Dec t So now we have a proposition in our type-level prolog called `DecEq` and some types, the ones with decidable equality, can instantiate it instance DecEq () where decEq _ _ = Yes refl -- Equality is symmetric, so is the negation of equality total negEqSym : {a : t} -> {b : t} -> (a = b -> _|_) -> (b = a -> _|_) negEqSym p h = p (sym h) -- Proof that zero isn't equal to any number greater than zero total OnotS : Z = S n -> _|_ OnotS refl impossible instance DecEq Nat where decEq Z Z = Yes refl decEq Z (S _) = No OnotS decEq (S _) Z = No (negEqSym OnotS) -- recurse on the arguments together and modify the eventual -- decided proof so as to match the arguments actually passed. -- -- I.e. we might find that Yes (n = m) but we need Yes (S n = S m) -- decEq (S n) (S m) with (decEq n m) | Yes p = Yes $ cong p | No p = No $ \h : (S n = S m) => p $ succInjective n m h Finally, at compile time Idris will try to infer the concrete types instantiating variables throughout the program. If any of the variables are bounded by `DecEq` then it must be able to solve the typeclass prolog to establish decidable equality for that type. If it fails to fulfill that obligation then it'll fail at compile time. -- this fails since functions on naturals are -- far, far, far from decidable... Idris cannot achieve the -- obligation to find `DecEq (Nat -> Nat)`. decEq : (x : Nat -> Nat) -> y -> Dec (x = y)
• lobster_johnson 12y ago
  Pascal, and Pascal-derived languages such as Modula and Turbo Pascal, have this: type Age = 1..199; A value of type Age can only have the values 1 <= x <= 199, and can't be assigned to non-Age variables. Enums belong to this category of ordinal types. In Ada: type Age is Range 1 .. 199; type Temperature is new Integer Range 32 .. 212; a: Age; t: Temperature a := t -- this fails at compile time Ada 2012 adds the support for specifying Eiffel-style contracts, but on types: subtype Even is Integer with Dynamic_Predicate => Even mod 2 = 0; You can't assign an odd number to a variable of type Even.
  • mamcx 12y ago
    Yep, I know about pascal (my 2d language after foxpro) but not the ADA 2012. The Dynamic_Predicate is on runtime or compile time? If assign a:Int = Even, I need to be explicit and do a convert (I imagine is yes, that is the pascal style but not have experience with ADA)
    • lobster_johnson 12y ago
      I believe it occurs only at compile time if it is possible for the compiler to evaluate the check; otherwise it's done at runtime.