Some questions

[Dirk Ullrich]

Hello all,

I have two questions about Idris.

1. How can I refer to `List's constructor `::' defined in
`prelude.list' without inferring it from the context?

Since the constructors `Nil' and `(::)' defined both for
`prelude.list' and `prelude.vect' Idris surely need some support (or
information form the context) to choose the right one. So I understand
that I get:

$ idris
Idris> :t Nil
No such variable Nil

but that the following works:

Idris> : t prelude.list.Nil
prelude.list.Nil : (a : Set) -> List a

But what's about `(::)'?

Idris> :t prelude.list.(::)
No such variable prelude.list.
Idris> :t (prelude.list.::)
Nothing to introduce
Idris> :t prelude.list.::
"(input)" (line 1, column 19):
unexpected end of input
expecting end of "::", "[", "if", "![", "?", "refl", "proof",
"tactics", "case", identifier, "instance", "(", "(|", "[|", "Integer",
"Int", "Char", "Float", "String", "Ptr", float, natural, literal
string, character, "Set", "()", "_|_", "_", "record", "\\", "let",
"|", "{" or "do"

2. When I give my own definition for `List' using the GADT notation:

$ cat mylist.idr
module mylist

data List : Set -> Set where
Nil : List A
(::) : A -> List A -> List A

infixr 10 ::

$ idris --noprelude mylist.idr
Type checking ./mylist.idr
*mylist> :t Nil
Nil : (A : Set) -> List A
*mylist> :t (::)
:: : (A : Set) -> A -> (List A) -> List A

So I get, for the type of my type constructors `Nil' and `(::)' a `(A
: Set)' argument for `List's parameter added. Well, if *I* myself add
such a type argument:

$ cat mylist2.idr
module mylist2

data List : Set -> Set where
Nil : (A : Set) -> List A
(::) : (A : Set) -> A -> List A -> List A

infixr 10 ::

$ idris --noprelude mylist2.idr
Type checking ./mylist2.idr
*mylist2> :t Nil
Nil : (A : Set) -> List A
*mylist2> :t (::)
:: : (A : Set) -> A -> (List A) -> List A
*mylist2> :t True :: Nil
((A : Set) -> List A) :: Nil : (List ((A : Set) -> List A)) -> List
((A : Set) -> List A)

The last type seems more plausible to me (if I suppose that, for type
constructors of a datatype, arguments for the datatype's parameters /
indexes are silently added), but what's about Idris' answers for `:t
Nil' and `:t (::)'?

Sorry for doing such useless things with Idris - but that's my way to
get some fine points
Dirk

[Edwin Brady]

On 8 Mar 2012, at 20:45, Dirk Ullrich wrote:

> Hello all,
>
> I have two questions about Idris.
>
> 1. How can I refer to `List's constructor `::' defined in
> `prelude.list' without inferring it from the context?

The short answer to this is "Oops, I haven't implemented that yet, sorry..."

Infix constructors are handled slightly differently by the parser and the namespace
disambiguation doesn't work for them. You could, perhaps, make a smart constructor
with an explicit type for the moment, but I will try to fix it properly soon.

> 2. When I give my own definition for `List' using the GADT notation:

> [...]

> The last type seems more plausible to me (if I suppose that, for type
> constructors of a datatype, arguments for the datatype's parameters /
> indexes are silently added), but what's about Idris' answers for `:t
> Nil' and `:t (::)'?

I'm less sure of what you're asking here... but I think the confusion may be caused by the REPL not printing implicit arguments helpfully. What is being reported is the type of the constructor in the core language (which doesn't have implicit syntax at all) rather than the type in the high level notation.

On the one hand, this is obviously a bug, because it's a confusing way to print things. On the other hand, it's a problem with the high level printing rather than type checking the core, which is always reassuring to me at least :).

> Sorry for doing such useless things with Idris - but that's my way to
> get some fine points

It's only by asking these small questions that I'll fix the minor things... so please do!

I don't know if I'll have time to fix things much in the next couple of weeks though - at least partly because I'm now deep into writing up the core language and the elaborator... of course that will hopefully make some of these questions easier to answer.

Edwin.

[Dirk Ullrich]

Hello Edwin

Am 8. März 2012 22:10 schrieb Edwin Brady <edwin...@gmail.com>:
> On 8 Mar 2012, at 20:45, Dirk Ullrich wrote:
>
>> Hello all,
>>
>> I have two questions about Idris.
>>
>> 1. How can I refer to `List's constructor `::' defined in
>> `prelude.list' without inferring it from the context?
>
> The short answer to this is "Oops, I haven't implemented that yet, sorry..."
>
> Infix constructors are handled slightly differently by the parser and the namespace
> disambiguation doesn't work for them. You could, perhaps, make a smart constructor
> with an explicit type for the moment, but I will try to fix it properly soon.

Nice to hear to finally get it fixed but I am not in a hurry ;-)

>
>> 2. When I give my own definition for `List' using the GADT notation:
>> [...]
>> The last type seems more plausible to me (if I suppose that, for type
>> constructors of a datatype, arguments for the datatype's parameters /
>> indexes are silently added), but what's about Idris' answers for `:t
>> Nil' and `:t (::)'?
>
> I'm less sure of what you're asking here... but I think the confusion may be caused by the REPL not printing implicit arguments helpfully. What is being reported is the type of the constructor in the core language (which doesn't have implicit syntax at all) rather than the type in the high level notation.

These are only experiments to properly understand what the fully
explicit types are (both in the high level language and in the core
language).

>
> On the one hand, this is obviously a bug, because it's a confusing way to print things. On the other hand, it's a problem with the high level printing rather than type checking the core, which is always reassuring to me at least :).

So, in high level notation, the type of the type constructors of
`List' in `mylist.idr' could be printed as
Nil : {A : Set} -> List A
(::) : {A : Set} -> A -> List A -> List A
?

>
>> Sorry for doing such useless things with Idris - but that's my way to
>> get some fine points
>
> It's only by asking these small questions that I'll fix the minor things... so please do!
>
> I don't know if I'll have time to fix things much in the next couple of weeks though - at least partly because I'm now deep into writing up the core language and the elaborator... of course that will hopefully make some of these questions easier to answer.

Yes. I've already noticed with pleasure that the implementation paper
is growing day by day since this one way to understand Idris'
principles and inner workings. I am very interested in that. One if
the reasons I like Idris for being - at least until now - not such a
heavy beast like, for instance, Coq or Agda. Smaller is better for
learning. And even better that it has this even smaller core language.
So I have a chance to understand these 'dependent type stuff'.
(The other reason for loving Idris is that it is meant to be a useful
programming language with full dependent types. I prefer this
wholehearted approach since for my understanding the current GHC
Haskell approach - adding zillion of subfeatures of fully dependent
types - is rather confusing.)

Dirk