dependent types and dispatch

[andrew cooke]

in a couple of places it says that julia's types are dependent.  does that mean that i can dispatch on values?  if so, how?

for example, i have a structure with some binary fields.  i would like to call different functions depending on whether those fields are set or not.

(since i am pretty sure this isn't possible, how are julia's types dependent?  maybe i have misunderstood what it means - i thought it meant that they included values.  the typical example is array size, isn't it?  maybe i am very confused....)

thanks,

andrew

[andrew cooke]

binary -> boolean

[Patrick O'Leary]

Dependent just means that types can be parameterized by a value; for example, Array{Float64,3} represents a three-dimensional array, with the second parameter being a value representing the number of dimensions. The types are not parameterized by *their* values, but by formal parameters of the type.

You're interested in pattern matching on types--you might want to check out https://github.com/toivoh/PatternDispatch.jl

[andrew cooke]

ah, thanks.

(i'm curious.  i'm no expert, but that's not very dependent then, is it?  looking at the wikipedia article, it seems to be similar to dependent ml (only) which "Some computer scientists do not consider [...] to be dependent"

http://en.wikipedia.org/wiki/Dependent_type

http://en.wikipedia.org/wiki/Dependent_ML ?  (genuinely curious here - don't have a cs degree, so am only going by what i read))

cheers,

andrew

[Matthias BUSSONNIER]

Le 15 nov. 2013 à 15:50, andrew cooke a écrit :

ah, thanks.

(i'm curious.  i'm no expert, but that's not very dependent then, is it?  looking at the wikipedia article, it seems to be similar to dependent ml (only) which "Some computer scientists do not consider [...] to be dependent"

http://en.wikipedia.org/wiki/Dependent_type

http://en.wikipedia.org/wiki/Dependent_ML ?  (genuinely curious here - don't have a cs degree, so am only going by what i read))

I think that Patrick example wasn't clear enough 

Array{T,N} is a type that depend on T and N

Array{Float64,3}

Here T is Float64 (another type)

and N, here 3

> In computer science and logic, a dependent type is a type that depends on a value.

So it looks like it matches this definition for me, and IIUC,  Dependant ML allow dependent type but only with Number.

(no cs background either, so not sure) 

--

Matthias

[Patrick O'Leary]

It may not be fully dependent in that the values we parameterize over aren't aribtrary, but then again Julia isn't total (we can write non-terminating programs) so I'm not sure that it could take full advantage of that power.

(A third non-CS voice in this conversation!)

But I can copy and paste a paragraph from the introduction of Norell and Chapman's "Dependently Typed Programming in Agda" [0].

"The standard example of a dependent type is the type of lists of a given length:

Vec A n. Here A is the type of the elements and n is the length of the list. Many languages allow you to define lists (or arrays) of a given size, but what makes Vec a true dependent type is that the length of the list can be an arbitrary term, which need not be known at compile time."

[0] http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf