Two much accuracy can actually be bad

[gmhwxi]

Today, I encountered a very interesting issue involving dependent types.

Say, I have a string "abcde". Then I can use the string to create a predicate P:

val P = fmemq("abcde"): bool

Given a char x, P(x) returns true if and only if x appears in the string "abcde".

What is the type for P?

In a non-dependent type system, P is usually given the type: (char) -> bool.

Given a sequence xs containing elements of type T, fmemq(xs) returns a function

of type (T) -> bool. For the string "abcde", this T is precisely the type for chars

ranging over "abcde". In other words, fmemq("abcde") is a function that can be applied

to a char c only if c appears in "abcde". This defeats the very need for fmemq("abcde"):

If it can ever be applied, then the application always returns true.

Have fun!

--Hongwei

But in a dependent type system,

[Brandon Barker]

But isn't this example similar to the idea of literal types?; defeating the need for such checks can avoid runtime costs as well as add specificity and safety to function signatures. Maybe I misunderstood some subtlety.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/61afb765-afe1-48be-a3fe-12e33b28b924o%40googlegroups.com.

[Dambaev Alexander]

Hi,

I am also think, that dependent/refinement types' purpose is to take a prove from a programmer, that one had checked once in runtime, that some variable satisfies some condition and then use that prove during compile time checks, thus eliminating requirement to use multiple runtime checks.

I think, that the example above is not too precise due to missing of context. Usually, you will have a function of type T -> bool to check condition in runtime, but dependent types allow you to encode property so it will be able to be checked in compile time.

Instead, I suggest to view an example of checking command line argument: say, that some app is able to handle arguments  "add" and "delete", then you can code some property P_delete(x) and P_add(x), so that some function delete will be like:

fn {cmd: string | P_delete(s)} delete( s string cmd, ...) = ...

and

fn {cmd: string | P_add(s)} add( s: string cmd, ...) = ...

such that you:

1. have to check for content of string once in runtime - you are not required to actually check it contents in delete() and add();

2. be sure, that you haven't used delete() when command is not delete().

The interesting question is: is it possible to not define argument ```s``` for both of those functions at all, as we know it's content/property already.

чт, 2 июл. 2020 г. в 21:52, Brandon Barker <brandon...@gmail.com>:

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAORbNRrQFH7hZtX17K9eEdjC2BQk85trMA8zm0_%2BZ7aGxpLGzw%40mail.gmail.com.

[gmhwxi]

Here is another way to see the issue I mentioned in my original message.

Say we have the following interface:

fun

<a:type>

fmemq(xs: list(a)): (a -> bool)

The function fmemq is supposed to turn a given list into a function that checks if a given

element is in the given list.

Suppose that we do

val foo = fmemq(xs) where { val xs = 1::2::3::nil() }

Say we infer a dependent type list(T) for the list xs where T = [a:int | a=1 || a=2 || a=3] int(a).

Note that T is the type precisely for the three integers 1, 2, and 3. Then the function foo is of

the type (T -> bool), which make foo not a very useful function. Why? Because foo is actually

a constant function that maps every integer in its domain to true. This is just an interesting example

showing that inferring the "most accurate" types may not actually be what the programmer really wants.

On Thursday, July 2, 2020 at 5:52:44 PM UTC-4, Brandon Barker wrote:

But isn't this example similar to the idea of literal types?; defeating the need for such checks can avoid runtime costs as well as add specificity and safety to function signatures. Maybe I misunderstood some subtlety.

On Thu, Jul 2, 2020, 4:51 PM gmhwxi <...> wrote:

Today, I encountered a very interesting issue involving dependent types.

Say, I have a string "abcde". Then I can use the string to create a predicate P:

val P = fmemq("abcde"): bool

Given a char x, P(x) returns true if and only if x appears in the string "abcde".

What is the type for P?

In a non-dependent type system, P is usually given the type: (char) -> bool.

Given a sequence xs containing elements of type T, fmemq(xs) returns a function

of type (T) -> bool. For the string "abcde", this T is precisely the type for chars

ranging over "abcde". In other words, fmemq("abcde") is a function that can be applied

to a char c only if c appears in "abcde". This defeats the very need for fmemq("abcde"):

If it can ever be applied, then the application always returns true.

Have fun!

--Hongwei

But in a dependent type system,

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.