Oplæg om dependent types i Idris

[David Christiansen]

Hej folks,

Undskyld på forhånd for evt kikset dansk - trods mit efternavn har jeg lært sproget som voksen.

Jeg er scala-entusiast, men ikke p.t. en særlig aktiv Scala-bruger da jeg arbejder på et projekt i Haskell. Jeg brugte dog Scala en hel del for et års tid siden, i forbindelse med et DSL projekt. Mit nuværende projekt er udvidelser af Edwin Brady's sprog Idris, som er et dependently-typed funktionssprog. Mest arbejder jeg på compileren, på faciliteter til praktisk programmering som fx noget i stil med F#'s type providers. I fremtiden vil jeg også arbejde på at udvide faciliteterne til DSL-indlejring.

Jeg hørte fra Mads at der har været interesse i dependent types i gruppen. Er I interesseret i et introduktion til dependent types som de ser ud i Idris? Det er ikke direkte Scala-relevant, men det virker som om en hel del idéer fra avanceret funktionsprogrammering er ved at finde indpas fx i Shapeless og Scalaz, og det er måske interessant at se, hvad der måske kommer om et par år samt at få en fornemmelse for nogle af de ting, som man laver i nye avancerede typesystemer.

Jeg kunne fx give en indledning i hvad dependent types er, hvorfor de er interessante, og hvad der er af udfordringer som vi skal løse før de kan bredes ud til det bredere industrikontekst.

Lyder det interessant for en fremtidig meetup?

/David

[Mads Hartmann Jensen]

Hej David,

Jeg er sevlfølgelig interesseret; prøvede selv at give et oplæg om det i torsdags men gik i stå da typerne ikke ville gå op.

Det næste arrangement er d. 8/11 men der fokuserer vi på Scala nybegyndere så vi kan få noget mere aktivitet i gruppen. Så der går det nok ikke at fortælle om dependent types ;)

Men efter d. 8. vil jeg meget gerne høre om dependent types

MVH,

Mads

[rvange]

Hej David

Meget interessant, og vil gerne høre mere. Jeg bor i Århus - kommer du til Goto i Århus i oktober? Der bliver vist nok et gratis oplæg i Scala brugergruppen fra en Scala entusiast fra The Guardian. Måske det kan kombineres med et oplæg fra dig? Jeg er ikke arrangør af hverken Goto eller Scala-arrangementet.

Venlig hilsen René

[Søren Mathiasen]

Hejsa,

Skal også til GOTO, har du et link til det arrangement med ham fra The Guardian ?

/Søren

On 09/09/2013, at 10.42, rvange <rene.va...@gmail.com>

 wrote:

--
You received this message because you are subscribed to the Google Groups "Scala User Group-Denmark" group.
To unsubscribe from this group and stop receiving emails from it, send an email to scala-user-group-d...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.

Med venlig hilsen / Best regards

SØREN MATHIASEN 
MOBIL: +45 4161 5667 
E-MAIL: SO...@SCHANTZ.COM

SCHANTZ A/S 
KIGKURREN 10 
DK-2300 København S
TLF. +45 3332 1984 
FAX +45 3332 1919 
WWW.SCHANTZ.COM

[rvange]

Steffen Egelund Jensen, som er primus motor på Scala-gruppen i Århus, har netop givet mig dette link: https://secure.trifork.com/aarhus-2013/freeevent/index.jsp?eventOID=5776

Den mandag den 9. september 2013 10.46.23 UTC+2 skrev Soren Mathiasen:

Hejsa,

Skal også til GOTO, har du et link til det arrangement med ham fra The Guardian ?

/Søren

On 09/09/2013, at 10.42, rvange <rene.va...@gmail.com>

 wrote:

Hej David

Meget interessant, og vil gerne høre mere. Jeg bor i Århus - kommer du til Goto i Århus i oktober? Der bliver vist nok et gratis oplæg i Scala brugergruppen fra en Scala entusiast fra The Guardian. Måske det kan kombineres med et oplæg fra dig? Jeg er ikke arrangør af hverken Goto eller Scala-arrangementet.

Venlig hilsen René

Den fredag den 6. september 2013 18.26.29 UTC+2 skrev David Christiansen:

Hej folks,

Undskyld på forhånd for evt kikset dansk - trods mit efternavn har jeg lært sproget som voksen.

Jeg er scala-entusiast, men ikke p.t. en særlig aktiv Scala-bruger da jeg arbejder på et projekt i Haskell. Jeg brugte dog Scala en hel del for et års tid siden, i forbindelse med et DSL projekt. Mit nuværende projekt er udvidelser af Edwin Brady's sprog Idris, som er et dependently-typed funktionssprog. Mest arbejder jeg på compileren, på faciliteter til praktisk programmering som fx noget i stil med F#'s type providers. I fremtiden vil jeg også arbejde på at udvide faciliteterne til DSL-indlejring.

Jeg hørte fra Mads at der har været interesse i dependent types i gruppen. Er I interesseret i et introduktion til dependent types som de ser ud i Idris? Det er ikke direkte Scala-relevant, men det virker som om en hel del idéer fra avanceret funktionsprogrammering er ved at finde indpas fx i Shapeless og Scalaz, og det er måske interessant at se, hvad der måske kommer om et par år samt at få en fornemmelse for nogle af de ting, som man laver i nye avancerede typesystemer.

Jeg kunne fx give en indledning i hvad dependent types er, hvorfor de er interessante, og hvad der er af udfordringer som vi skal løse før de kan bredes ud til det bredere industrikontekst.

Lyder det interessant for en fremtidig meetup?

/David

--
You received this message because you are subscribed to the Google Groups "Scala User Group-Denmark" group.

To unsubscribe from this group and stop receiving emails from it, send an email to scala-user-group-denmark+unsub...@googlegroups.com.

For more options, visit https://groups.google.com/groups/opt_out.

[David Christiansen]

Hej René

Jeg kommer ikke med til GOTO - har rigeligt met rejse i år! Jeg kommer
faktisk først tilbage fra ICFP midt i GOTO.

Men det lyder som om, at folk er interesseret i et Idrisoplæg herovre
i KBH. Det kommer nok ud på listen på et tidspunkt.

/David

> --
> You received this message because you are subscribed to the Google Groups
> "Scala User Group-Denmark" group.
> To unsubscribe from this group and stop receiving emails from it, send an

> email to scala-user-group-d...@googlegroups.com.