We have an opening for a PhD student in dependent type theory and
functional programming at Chalmers. Here is an excerpt from the ad:
The PhD student will join the Programming Logic group and contribute
to its research on dependent type theory and functional programming.
Topics of interest
==
VACANCY : 1x Phd position in dependent types, testing hardware design
==
The research group of Software Technology is part of the Software
Systems division
#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
--+-
Reporter: Lemming | Owner:
Type
#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
+---
Reporter: Lemming | Owner
#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
+---
Reporter: Lemming | Owner
#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
+---
Reporter: Lemming | Owner
#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
+---
Reporter: Lemming | Owner
#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
+---
Reporter: Lemming | Owner
#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
+---
Reporter: Lemming | Owner
#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
+---
Reporter: Lemming | Owner
#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
+---
Reporter: Lemming | Owner
#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
+---
Reporter: Lemming | Owner
#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
+---
Reporter: Lemming | Owner
#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
---+
Reporter: Lemming| Owner
Hello,
in a Haskell development I have to represent paths that have elements of
alternating types. GADTs allow me to do this easily:
data AltList :: * - * - * where
Nil :: AltList a a
ICons :: Int - AltList Int b - AltList () b
UCons :: () - AltList () b - AltList Int b
Since I have
Hi
This has been discussed here[1] and here[2], and the answer is that
its not possible because of making type inference generally
impossible. It would be a useful feature though, and could be
implemented by requiring the user give additional type signatures to
help the inference algorithm out.
Will this help?
data List a b where
List :: [a] - List a a
05.01.2012, в 17:12, Robbert Krebbers mailingli...@robbertkrebbers.nl
написал(а):
Hello,
in a Haskell development I have to represent paths that have elements of
alternating types. GADTs allow me to do this easily:
data
Hi Eugene,
with respect to typing your solution is a lot nicer since the type
arguments are not just ignored. But apart from that it does not help too
much in the below example, since it does not allow me to get rid of the
additional constructor (List in your case, IntList in mine) and it
be no new variables on the RHS.
So CD permits function to be defined and prohibits general assertions
which are more in the domain of a specification language.
Question 1: Is the above a reasonable understanding of CD?
Question 2: I have read that the lack of dependent types (DT) prevents
writing
On 17 July 2011 10:03, Patrick Browne patrick.bro...@dit.ie wrote:
Question 1: Is the above a reasonable understanding of CD?
From a brief look, constructor discipline (CD) restricts left-hand
sides of equations to have no function calls themselves.
Hello,
Here is probably a good paper to get people up to speed on dependent
types (ironically written by two contributors to this mailing list??):
okmij.org/ftp/papers/lightweight-static-capabilities.pdf
Vasili
___
Haskell-Cafe mailing list
On Saturday 19 February 2011 1:11:23 AM Vasili I. Galchin wrote:
BTW I was thinking of http://www.ats.org when I asked this question.
Technically speaking, if one considers ATS to be dependently typed, then one
might as well also consider GHC to be dependently typed (with the right
extensions
Hello,
Does Haskell currently have support for linear types and dependent
types? If so, is it necessary to specify a pragma to use and if so, what
is the pragma(s)?
Kind regards,
Vasili
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
vigalchin:
Hello,
�� Does Haskell currently have support for linear types and dependent
types?
No.
-- Don
P.S. :-)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
On 18 February 2011 20:04, Vasili I. Galchin vigalc...@gmail.com wrote:
Does Haskell currently have support for linear types and dependent
types? If so, is it necessary to specify a pragma to use and if so, what
is the pragma(s)?
While Haskell doesn't have full dependent types, as found
for linear types and dependent
types? If so, is it necessary to specify a pragma to use and if so,
what
is the pragma(s)?
While Haskell doesn't have full dependent types, as found in say Agda,
it (or rather GHC) does have some extensions that allow you to get
many of the advantages of full
There has been extensive discussion of whether Haskell has dependent
types, made larger by the fact that the definition of
dependently-typed languages is a bit fuzzy. On some accounts, type
functions or GADTs are sufficient for calling a language
dependently-typed, and Haskell got both features
, I was studying how cartesian closed categories can be used to
describe typed functional languages. Types are objects and morphisms are
functions from one type to another.
Since I'm also interested in systems with dependent types, I wonder if
there is a categorical description of such systems
the (sum-product) version, but it is all largely a
matter of taste.
The product=function,sum=pair terminology comes from a certain
interpretation of dependent types in set theory. I believe this
originated with Per Martin-Löf's work, though I don't have any citations
on hand.
That terminology
Hi,
recently, I was studying how cartesian closed categories can be used to
describe typed functional languages. Types are objects and morphisms are
functions from one type to another.
Since I'm also interested in systems with dependent types, I wonder if
there is a categorical description
On 12/02/10 09:13, Petr Pudlak wrote:
Hi,
recently, I was studying how cartesian closed categories can be used to
describe typed functional languages. Types are objects and morphisms are
functions from one type to another.
Since I'm also interested in systems with dependent types, I
On Thu, 2 Dec 2010, Petr Pudlak wrote:
Hi,
recently, I was studying how cartesian closed categories can be used to
describe typed functional languages. Types are objects and morphisms are
functions from one type to another.
Since I'm also interested in systems with dependent types, I
Hi,
Bart Jacobs's book Categorical Logic and Type Theory has a
categorical description of a system with dependent types (among
others). The book is fairly advanced but it has lots of details about
the constructions.
Hope this helps,
-Iavor
On Thu, Dec 2, 2010 at 8:18 AM, rocon...@theorem.ca
On 12/02/10 11:19, Iavor Diatchki wrote:
Hi,
Bart Jacobs's book Categorical Logic and Type Theory has a
categorical description of a system with dependent types (among
others). The book is fairly advanced but it has lots of details about
the constructions.
Hope this helps,
-Iavor
Page
with dependent types, I wonder if
there is a categorical description of such systems. The problem (as I
see it) is that the codomain of a function depends on a value passed to
the function.
I'd happy if someone could give me some pointers to some papers or other
literature.
There are many
a
matter of taste.
-Iavor
On Thu, Dec 2, 2010 at 11:03 AM, Larry Evans cppljev...@suddenlink.net wrote:
On 12/02/10 11:19, Iavor Diatchki wrote:
Hi,
Bart Jacobs's book Categorical Logic and Type Theory has a
categorical description of a system with dependent types (among
others). The book
On 12/02/10 15:47, Iavor Diatchki wrote:
Hi,
You have it exactly right, and I don't think that there's a
particularly deep reason to prefer the one over the other. It seems
that computer science people
tend to go with the (product-function) terminology, while math people
seem to prefer the
On Thursday 02 December 2010 7:54:18 pm Larry Evans wrote:
[snip]
*Maybe* the computer science people are trying to minimize the concepts.
In this case, the one concept common to both the sum and product ( in
the math peoples viewpoint) is there's a function:
field2type: field_name -
Hi!
I believe dependent types is the right term for my problem. I was
trying to solve it with GADTs but I was not successful so I am turning
to infinite (lazy) wisdom of Haskell Cafe.
I am attaching example code where I had to define MaybePacket data
type which combines different types
On 10 September 2010 07:14, Mitar mmi...@gmail.com wrote:
But I am not sure how. Because now compiler, for example, warns me of
a non-exhaustive pattern even if some MaybePacket value is not
possible for given Line.
This issue pops up quite quite often - Ryan Ingram's answer to it the
last
Hi!
On Fri, Sep 10, 2010 at 9:22 AM, Stephen Tetley
stephen.tet...@gmail.com wrote:
This issue pops up quite quite often - Ryan Ingram's answer to it the
last time it was on the Cafe points to the relevant Trac issue
numbers:
But I have not yet made it as GADTs. I would need some help here.
Hi!
I made it. ;-)
Thanks to all help from copumpkin on IRC channel.
I am attaching my solution for similar problems in future. And of
course comments.
Mitar
Test5.hs
Description: Binary data
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
On Sun, Apr 11, 2010 at 10:54 PM, Jason Dagit da...@codersbase.com wrote:
Or, you could use witness types:
data Vehicle classification = Vehicle { ... }
mkCar :: Vehicle Car
mkTruck :: Vehicle Truck
Then you would export the smart constructors, (mkCar/mkTruck) without
exporting the Vehicle
On Mon, Apr 12, 2010 at 4:32 AM, Ben Millwood hask...@benmachine.co.ukwrote:
Personally I think this approach is all rather OO. The way that seems
most natural to me is:
moveVehicleAcrossBridge :: Bridge - Vehicle - Maybe Move
moveVehicleAcrossBridge bridge { maxWeight = max } vehicle {
On Sun, Apr 11, 2010 at 5:54 PM, Jason Dagit da...@codersbase.com wrote:
On Sun, Apr 11, 2010 at 1:59 AM, Andrew U. Frank
fr...@geoinfo.tuwien.ac.at wrote:
in modeling real application we have often the case that the type of
some object depends on a value. e.g. small_boat is a vessel with
On Mon, 2010-04-12 at 12:44 -0400, Anthony Cowley wrote:
On Sun, Apr 11, 2010 at 5:54 PM, Jason Dagit da...@codersbase.com wrote:
On Sun, Apr 11, 2010 at 1:59 AM, Andrew U. Frank
fr...@geoinfo.tuwien.ac.at wrote:
in modeling real application we have often the case that the type of
some
in modeling real application we have often the case that the type of
some object depends on a value. e.g. small_boat is a vessel with size
less than a constant. big_boat is a vessel with a larger size. for
example, many legal classifications are expressed in this form (e.g. car
vs. truck)
On Sun, 2010-04-11 at 10:59 +0200, Andrew U. Frank wrote:
in modeling real application we have often the case that the type of
some object depends on a value. e.g. small_boat is a vessel with size
less than a constant. big_boat is a vessel with a larger size. for
example, many legal
On Sun, Apr 11, 2010 at 1:59 AM, Andrew U. Frank fr...@geoinfo.tuwien.ac.at
wrote:
in modeling real application we have often the case that the type of
some object depends on a value. e.g. small_boat is a vessel with size
less than a constant. big_boat is a vessel with a larger size. for
On 11 April 2010 22:54, Jason Dagit da...@codersbase.com wrote:
...
class Vehicle a where
data Car
data Truck
instance Vehicle Car where
instance Vehicle Truck where
Now you can have things that take a Car or a Truck or they can take a
Vehicle instead.
moveVehicle :: Vehicle v = v
On Sun, Apr 11, 2010 at 4:15 PM, Ozgur Akgun ozgurak...@gmail.com wrote:
On 11 April 2010 22:54, Jason Dagit da...@codersbase.com wrote:
...
class Vehicle a where
data Car
data Truck
instance Vehicle Car where
instance Vehicle Truck where
Now you can have things that take a Car
pbrowne wrote:
Dependent Types (DT)
The purpose of dependent types (DT) is to allow programmers to specify
dependencies between the parameters of a multiple parameter class.
'Dependent type' means result type (of a function) can depend on argument
values. This is not (directly) supported
of a
class. Note, the notion of FD is distinct from the concept of 'Dependent
types', where the result type (of a function) can depend on argument values.
FD are declared in a class header, where the type of one class
parameter is declared to depend on another class parameter. Consider the
following
Hi,
I am attempting to explain an example of dependent types to computing
practitioners who do not have any background in functional programming.
My goal is to explain the example rather than implement or improve it. I
have been told in previous postings that the approach below is a bit
dated. Any
://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.4391
and ftp://ftp.cs.kun.nl/pub/CompMath.Found/HBKJ.ps.Z
On Fri, Oct 09, 2009 at 02:11:30PM +0100, pat browne wrote:
Hi,
I am trying to understand the concept of dependent types as described in
Haskell literature (Hallgren 2001),(Hinze
, so take it with salt.
I am aware that dependent types can be used to express constraints on
the size of lists and other collections.
Technically, you don't need dependent types for this, you just need type-level
naturals. But dependent types (or some sufficiently fancy faking thereof
Hi,
I am trying to understand the concept of dependent types as described in
Haskell literature (Hallgren 2001),(Hinze,Jeuring et al. 2006). I am
particularly interested in understanding two flavours of dependency
mentioned by Hinze et al:
1) Types depending on values called dependent types
2
are:
Question 1: Is my understanding correct?
Question 2: What flavour of DT is this does this example exhibit?
When you say Dependent Types, what is usually meant is that types can
depend on *values*; for example:
data Vector :: Integer - * - * where
Nil :: Vector 0 a
Cons :: a - Vector n
do not break parametricity
for *unordered sets* (as opposed to lists) - turns out, not too many.
2009/5/18 Conor McBride co...@strictlypositive.org:
Hi
Questions of parametricity in dependent types are made more
complex by the way in which the Pi-type
(x : S) - T
corresponds to universal
Thanks, at least the title looks like exactly what I've been looking
for, however I cannot quickly appreciate the notation-heavy contents:
I definitely will as soon as possible.
2009/5/20 Masahiro Sakai masahiro.sa...@gmail.com:
From: Eugene Kirpichov ekirpic...@gmail.com
Date: Sun, 17 May 2009
Hi
On 20 May 2009, at 07:08, Eugene Kirpichov wrote:
Thanks for the thorough response.
I've found BarrasBernardo's work (at least, slides) about ICC*, I'll
have a look at it.
Could you provide with names of works by Altenkirch/Morris/Oury/you?
The unordered pair example was especially
Or in a language without bottoms.
2009/5/20 David Menendez d...@zednenem.com:
On Sun, May 17, 2009 at 11:52 PM, Ryan Ingram ryani.s...@gmail.com wrote:
Free theorem's are theorems about functions that rely only on parametricity.
For example, consider any function f with the type
forall a.
On Sun, May 17, 2009 at 11:52 PM, Ryan Ingram ryani.s...@gmail.com wrote:
Free theorem's are theorems about functions that rely only on parametricity.
For example, consider any function f with the type
forall a. a - a
From its type, I can tell you directly that this theorem holds:
forall
From: Eugene Kirpichov ekirpic...@gmail.com
Date: Sun, 17 May 2009 23:10:12 +0400
Is there any research on applying free theorems / parametricity to
type systems more complex than System F; namely, Fomega, or calculus
of constructions and alike?
You may be interested in this:
The Theory of
Hi
Questions of parametricity in dependent types are made more
complex by the way in which the Pi-type
(x : S) - T
corresponds to universal quantification. It's good to think
of this type as a very large product, tupling up individual
T's for each possible x you can distinguish
could
possibly be a lot more powerful if there were a way to encode in the
type of 'sort' that it accepts a reflexive transitive antisymmetric
predicate, but the only way to express that is with dependent types.
Looks like the only thing one needs to add to System F is the
relational translation
master's thesis, the
final version of which is not quite ready yet.
Basically, free theorems in the Calculus of Constructions can be
substantially more complicated, because they have to exclude certain
dependent types in order to be valid. So much so that I do not think
that they are necessarily
in the Calculus of Constructions can be
substantially more complicated, because they have to exclude certain
dependent types in order to be valid. So much so that I do not think
that they are necessarily worthwhile to use in proofs. But that is just
an intuition, and I have not done enough different kinds
a reflexive transitive antisymmetric
predicate, but the only way to express that is with dependent types.
Looks like the only thing one needs to add to System F is the
relational translation rule for a dependent product; but I haven't
tried doing it myself.
begin:vcard
fn:Joseph Fredette
::(a-a-Bool)-[a]-[a]'. The theorem could
possibly be a lot more powerful if there were a way to encode in the
type of 'sort' that it accepts a reflexive transitive antisymmetric
predicate, but the only way to express that is with dependent types.
Looks like the only thing one needs to add to System F
I'm trying to understand how to use GADT types to simulate dependent
types. I'm trying to write a version of list that uses Peano numbers
in the types to keep track of how many elements are in the list. Like this:
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
module Plist
Am Samstag, 28. Juni 2008 19:51 schrieb Paul Johnson:
I'm trying to understand how to use GADT types to simulate dependent
types. I'm trying to write a version of list that uses Peano numbers
in the types to keep track of how many elements are in the list. Like
this:
{-# OPTIONS -fglasgow
On Saturday 28 June 2008, Paul Johnson wrote:
I'm trying to understand how to use GADT types to simulate dependent
types. I'm trying to write a version of list that uses Peano numbers
in the types to keep track of how many elements are in the list. Like
this:
{-# OPTIONS -fglasgow-exts
Daniel Fischer wrote:
My Oleg rating isn't high either, and certainly you can do it more elegant,
but
class Concat l1 l2 l3 | l1 l2 - l3, l1 l3 - l2 where
pConcat :: l1 a - l2 a - l3 a
instance Concat (Plist Zero) (Plist n) (Plist n) where
pConcat _ ys = ys
instance Concat (Plist
This library provides an implementation of parameterized types using
type-level computations to implement the type parameters and emulate
dependent types.
Right now only fixed-sized vectors are provided (based on Oleg's
Number-parameterized types [1] and Frederik Eaton's Vectro library
[2
DavidA wrote:
Twan van Laarhoven twanvl at gmail.com writes:
The solution is to use a dummy parameter:
class IntegerType a where
value :: a - Integer
Thanks to all respondents for this suggestion. That works great.
I prefer a slightly elaborate way,
newtype Mark n t = Mark t
)
The problem with this approach is that it's not really type-safe:
I can attempt to add a + b sqrt 2 to c + d sqrt 3, whereas this should be a
type error because 2 /= 3.
So I thought I'd have a go at doing it with phantom types. In effect I'd be
using phantom types to simulate dependent types
it with phantom types. In effect I'd
be
using phantom types to simulate dependent types. Here's the code:
{-# OPTIONS_GHC -fglasgow-exts #-}
import Data.Ratio
class IntegerType a where
value :: Integer
data Two
instance IntegerType Two where value = 2
data Three
instance IntegerType Three
DavidA wrote:
Hi,
I am trying to implement quadratic fields Q(sqrt d). These are numbers of the
form a + b sqrt d, where a and b are rationals, and d is an integer.
...
class IntegerType a where
value :: Integer
The problem is, this doesn't work. GHC complains:
The class method
Twan van Laarhoven twanvl at gmail.com writes:
The solution is to use a dummy parameter:
class IntegerType a where
value :: a - Integer
And call it like:
f = value (undefined :: Two)
So for instance:
instance IntegerType d = Show (QF d) where
show (QF a b) = show a ++
Hello,
As the authors point out [1], coal-face time needs to be expended before
real world adoption of Dependently-Typed functional programming. But let's
get the ball rolling. They say that haskell programmers are normally averse
to dependent types. Is this true? It seems to me that one
averse
to dependent types. Is this true? It seems to me that one of the appeals
of Haskell is the ability to program in a prove perfect, write once
(elegant) style. Is not dependent typing a good move towards this goal?.
It addresses a problem [2] with which we, in our everyday common
inter
averse
to dependent types. Is this true? It seems to me that one of the appeals
of Haskell is the ability to program in a prove perfect, write once
(elegant) style. Is not dependent typing a good move towards this goal?.
It addresses a problem [2] with which we, in our everyday common
inter
: given the expression, we
compute its type -- or report a failure if the expression is
ill-typed. That is, the result *type* Term a is a function of the
*value* Expr. Thus is truly a problem of dependent types. And Haskell
is up to it: Haskell is genuinely a dependently typed language.
We show
[EMAIL PROTECTED] wrote:
Greg Buchholz has posed an interesting problem of writing a
typechecker. Given untyped terms of the form
...snip...
We show the solution that uses no GADTs and no representation types.
We retain however the eval function in the previous message that uses
GADT. Our
An earlier message showed an example of writing code with non-trivial
static guarantees in the present-day Haskell (i.e., Haskell98 + rank-2
types).
http://pobox.com/~oleg/ftp/Haskell/types.html#branding
Although this approach obviously falls short of the genuine dependent
typing, we
I think you are confusing Dependent Types with Functional Dependencies.
Actually the two are not that dissimilar... If we allow types to depend
on types (which is what Functional Dependencies allow) IE:
class a b | a - b
instance Int Float
instance Float Int
For example
On Fri, Aug 27, 2004 at 10:26:51AM -0400, Michael Manti wrote:
I recognize that I'm far out of my depth here--both in Haskell and in
mathematics--but I'll ask anyway. In what ways are dependent types
(http://haskell.org/hawiki/FunDeps,
http://www.cse.ogi.edu/~mpj/pubs/fundeps.html
occuring dependent types in
mathematics. Variable names for polynomials, expansion point and 'scale'
for generalized series expansions, coefficient ring for normalization and
factorization of polynomials, and so on up the food chain. The dependencies
get quite interesting when one is dealing
I recognize that I'm far out of my depth here--both in Haskell and in mathematics--but
I'll ask anyway. In what ways are dependent types (http://haskell.org/hawiki/FunDeps,
http://www.cse.ogi.edu/~mpj/pubs/fundeps.html) insufficient to address these issues?
On Friday, August 27, 2004, at 10
Martin Sulzmann stated the goal of the append exercise as follows:
] Each list carries now some information about its length.
] The type annotation states that the sum of the output list
] is the sum of the two input lists.
I'd like to give a Haskell implementation of such an append
function,
There's a potentially confusing typo.
append Nil ys = Nil
should be replaced by
append Nil ys = ys
Thanks to Ketil for pointing this out.
Martin
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
Just a couple of quick points...
Why store the length along with the list, the length is stored
using type level naturals (Succ | Zero) but these are identical
to the recursion pattern in a List (Cons | Nil) - therefore it
is no less work than having a length function which converts
from one to
Actually the data statement wasnt quite right:
data Cons a b = Cons a b
Would work, but now there is nothing keeping each
element in the list as the same type,
I guess we could add a class to constrain to a normal list,,,
class List l x
instance List Nil x
instance List l x = List (Cons x l) x
The append example is meant to make a general point about
the connection between dependent types and Haskell with
extensions.
I know that the example itself is rather trivial, and
DML/index types, Omega, Haskell+GAD and Chameleon might
seem as too big canons for a rather small target.
Second
Hi Martin
Martin Sulzmann wrote:
Hi,
Inspired by Conor's and Oleg's discussion let's see which
dependent types properties can be expressed in Haskell (and extensions).
I use a very simple running example.
[..]
We'd like to statically guarantee that the sum of the output list
is the sum of the two
This will only work for terminating programs!
Interesting point, but thats because all the operations are at
the type level - therefore if a type is unknown at compile time
we cannot produce a program.
With this type class stuff values can depend on types, but
not the other way around. You can
Hi,
Inspired by Conor's and Oleg's discussion let's see which
dependent types properties can be expressed in Haskell (and extensions).
I use a very simple running example.
-- append.hs
-- append in Haskell
data List a = Nil
| Cons a (List a)
append :: List a - List a - List
.
The abstract `brand' is just a type-level proxy for the bounding
interval, and the library of operations provides interval-respecting
operations on indices. This is a very neat solution in Haskell, but it
goes round an extra corner which isn't necessary with dependent types,
where you can just talk about
Hello!
Bjorn Lisper wrote:
What is the relation to the sized types by Lars Pareto and John Hughes?
It is orthogonal and complementary, as the message in response to
Conor T. McBride indicated.
What is the relation to classical range analyses for (e.g.) array index
expressions, which have
1 - 100 of 182 matches
Mail list logo
