[Caml-list] First-Class Types?!

[Caml-list] First-Class Types?!

[Oliver Bandel]

Hello,

will there be first-class types in OCaml one day?

GADT and first-class-modules as a first step towards
first-class-types?

Is it planned?
Is it possible in OCaml at all?


Ciao,
    Oliver

Re: [Caml-list] First-Class Types?!

[Oliver Bandel]

Zitat von Oliver Bandel <oliver@first.in-berlin.de> (Tue, 11 Oct 2016  
23:55:21 +0200)

> Hello,
>
> will there be first-class types in OCaml one day?
[...]

Meaning: types as first-class values...


Ciao,
    Oliver

Re: [Caml-list] First-Class Types?!

[Oliver Bandel]

Zitat von Oliver Bandel <oliver@first.in-berlin.de> (Tue, 11 Oct 2016  
23:57:48 +0200)

> Zitat von Oliver Bandel <oliver@first.in-berlin.de> (Tue, 11 Oct  
> 2016 23:55:21 +0200)
>
>> Hello,
>>
>> will there be first-class types in OCaml one day?
> [...]
>
> Meaning: types as first-class values...


...or does static types contradict first-class types?


Ciao,
    Oliver

Re: [Caml-list] First-Class Types?!

[Ivan Gotovchits]

> On Oct 11, 2016, at 6:20 PM, Oliver Bandel <oliver@first.in-berlin.de> wrote:
> 
> 
> Zitat von Oliver Bandel <oliver@first.in-berlin.de> (Tue, 11 Oct 2016 23:57:48 +0200)
> 
>> Zitat von Oliver Bandel <oliver@first.in-berlin.de> (Tue, 11 Oct 2016 23:55:21 +0200)
>> 
>>> Hello,
>>> 
>>> will there be first-class types in OCaml one day?

OCaml with first-class types is called Coq. 

>> [...]
>> 
>> Meaning: types as first-class values...
> 
> 
> ...or does static types contradict first-class types?

They do not… once you have decided what is the type of type, and should it be first class too :)



> 
> Ciao,
>   Oliver
> 
> 
> -- 
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

Re: [Caml-list] First-Class Types?!

[Oleg]

Currently MetaOCaml does not allow struct ... end and sig ... end
to appear within brackets. If it did, it becomes legitimate to talk
about splices not only within expressions but also type definitions,
etc. So, the notion of first-class types arises quite naturally once
we considered staging.

We have tried to contemplate this question and what good might
first-class types do. One immediate benefit would be specializing
functor applications and reducing/removing overhead of using
functors. When we thought about it further, it turns out we can do
essentially the same in existing (Meta)OCaml. Hence the problem: we
couldn't come up with a compelling example why we would need to extend
staging to type expressions. You can read more details in the PEPM
2016 paper

        http://okmij.org/ftp/meta-programming/StagingNG.pdf

Re: [Caml-list] First-Class Types?!

[Kakadu]

Which languages already have first class types? Where can I read about it?

Kakadu

On Wed, Oct 12, 2016 at 12:55 AM, Oliver Bandel
<oliver@first.in-berlin.de> wrote:
> Hello,
>
> will there be first-class types in OCaml one day?
>
> GADT and first-class-modules as a first step towards
> first-class-types?
>
> Is it planned?
> Is it possible in OCaml at all?
>
>
> Ciao,
>    Oliver
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

Re: [Caml-list] First-Class Types?!

[Haoyang Wang]

> On Oct 12, 2016, at 12:07 AM, Kakadu <kakadu.hafanana@gmail.com> wrote:
> Which languages already have first class types? Where can I read about it?

Coq https://coq.inria.fr

See also https://en.wikipedia.org/wiki/Lambda_cube

Haoyang

Re: [Caml-list] First-Class Types?!

[Oliver Bandel]

Aldor has first class types.
Aldor was developed as add-non language for the AXIOM-CAS.


Aldor:
   http://www.aldor.org/


AXIOM:
   http://axiom-developer.org/


Ciao,
    Oliver


Zitat von Kakadu <kakadu.hafanana@gmail.com> (Wed, 12 Oct 2016 10:07:27 +0300)

> Which languages already have first class types? Where can I read about it?
>
> Kakadu
>
> On Wed, Oct 12, 2016 at 12:55 AM, Oliver Bandel
> <oliver@first.in-berlin.de> wrote:
>> Hello,
>>
>> will there be first-class types in OCaml one day?
>>
>> GADT and first-class-modules as a first step towards
>> first-class-types?
>>
>> Is it planned?
>> Is it possible in OCaml at all?
>>
>>
>> Ciao,
>>    Oliver
>>
>>
>> --
>> Caml-list mailing list.  Subscription management and archives:
>> https://sympa.inria.fr/sympa/arc/caml-list
>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>> Bug reports: http://caml.inria.fr/bin/caml-bugs