Andrew Coppin wrote:
wren ng thornton wrote:
Andrew Coppin wrote:
It's a bit like trying to learn Prolog from somebody who thinks that
the difference between first-order and second-order logic is somehow
common knowledge. (FWIW, I have absolutely no clue what that
difference is.
Andrew Coppin wrote:
I did wonder what the heck a type function is or why you'd want one.
And then a while later I wrote some code along the lines of
class Collection c where
type Element c :: *
empty :: c - Bool
first :: c - Element c
So now it's like Element is a function that
On Fri, Jun 25, 2010 at 02:26:54PM -0700, Walt Rorie-Baety wrote:
I've noticed over the - okay, over the months - that some folks enjoy the
puzzle-like qualities of programming in the type system (poor Oleg, he's
become #haskell's answer to the Chuck Norris meme commonly encountered in
So is there a specific reason why Haskell isn't dependently typed then?
Or you could ask, So is there a specific reason why C isn't a functional
language?
More to the point, Haskell was a bit too frozen in stone when dependent type
theory reached the point of being implementable.
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
On 6/28/10 15:04 , Andrew Coppin wrote:
More to the point, Haskell was a bit too frozen in stone when dependent type
theory reached the point of being implementable.
Right. So, in summary, the answer is historical circumstance?
(I was
wren ng thornton wrote:
Andrew Coppin wrote:
I think I looked at Coq (or was it Epigram?) and found it utterly
incomprehensible. Whoever wrote the document I was reading was
obviously very comfortable with advanced mathematical abstractions
which I've never even heard of.
One of the things
Brent Yorgey wrote:
As several people have pointed out, type-level programming in Haskell
resembles logic programming a la Prolog -- however, this actually only
applies to type-level programming using multi-parameter type classes
with functional dependencies [1] (which was until recently the
wren ng thornton wrote:
And, as Jason said, if you're just interested in having the same
programming style at both term and type levels, then you should look
into dependently typed languages.
Out of curiosity, what the hell does dependently typed mean anyway?
On 26 June 2010 08:07, Andrew Coppin andrewcop...@btinternet.com wrote:
Out of curiosity, what the hell does dependently typed mean anyway?
How about:
The result type of a function may depend on the argument value
(rather than just the argument type)
The quoted bit rather than the parens bit
It means that not only can values have types, types can have values.
An example of the uses of a dependent type would be to encode the
length of a list in it's type.
Due to the curry-howard isomorphism, dependent types open the gateway
for lots of type-level theorem proving.
On 26 June 2010
On Sat, Jun 26, 2010 at 12:07 AM, Andrew Coppin andrewcop...@btinternet.com
wrote:
wren ng thornton wrote:
And, as Jason said, if you're just interested in having the same
programming style at both term and type levels, then you should look into
dependently typed languages.
Out of
On Sat, Jun 26, 2010 at 12:27 AM, Jason Dagit da...@codersbase.com wrote:
On Sat, Jun 26, 2010 at 12:07 AM, Andrew Coppin
andrewcop...@btinternet.com wrote:
wren ng thornton wrote:
And, as Jason said, if you're just interested in having the same
programming style at both term and type
Liam O'Connor wrote:
It means that not only can values have types, types can have values.
Uh, don't types have values *now*?
An example of the uses of a dependent type would be to encode the
length of a list in it's type.
Oh, right. So you mean that as well as being able to say Foo
http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf
Andrew Coppin wrote:
Liam O'Connor wrote:
It means that not only can values have types, types can have values.
Uh, don't types have values *now*?
An example of the uses of a dependent type would be to encode the
length of a list in it's type.
Jason Dagit wrote:
On Sat, Jun 26, 2010 at 12:07 AM, Andrew Coppin
andrewcop...@btinternet.com mailto:andrewcop...@btinternet.com wrote:
Out of curiosity, what the hell does dependently typed mean anyway?
The types can depend on values. For example, have you ever notice we
have
Tony Morris wrote:
http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf
Ah yes, it was definitely Epigram I looked at. The intro to this looked
promising, but by about 3 pages in, I had absolutely no clue what on
Earth the text is talking about...
___
On Sat, Jun 26, 2010 at 3:49 AM, wren ng thornton w...@freegeek.org wrote:
Jason Dagit wrote:
On Fri, Jun 25, 2010 at 2:26 PM, Walt Rorie-Baety
black.m...@gmail.comwrote:
I've noticed over the - okay, over the months - that some folks enjoy the
puzzle-like qualities of programming in the
Hello Gábor,
Saturday, June 26, 2010, 4:29:28 PM, you wrote:
It's interesting how C++ is imperative at the term level and
functional at the type level
or logic? it supports indeterminate choice
--
Best regards,
Bulatmailto:bulat.zigans...@gmail.com
I prefer Agda to Epigram, but different strokes for different folks.
In agda, you could define a list indexed by its size like this:
data Vec : (A : Set) → ℕ → Set where
[] : Vec A 0
_∷_ : ∀ {n : ℕ} → A → Vec A n → Vec A (1 + n)
So, we have a Vec data type, and on the type level it is a
We most certainly do have type-level functions. See type families.
Cheers.
~Liam
On 26 June 2010 17:33, Jason Dagit da...@codersbase.com wrote:
On Sat, Jun 26, 2010 at 12:27 AM, Jason Dagit da...@codersbase.com wrote:
On Sat, Jun 26, 2010 at 12:07 AM, Andrew Coppin
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
On 6/26/10 07:28 , Andrew Coppin wrote:
Uh, don't types have values *now*?
To the extent that's true now, they're baked in; you can't do anything
to/with them.
Oh, right. So you mean that as well as being able to say Foo Bar, you can
say Foo 7,
On Sat, Jun 26, 2010 at 3:27 AM, Jason Dagit da...@codersbase.com wrote:
The types can depend on values. For example, have you ever notice we have
families of functions in Haskell like zip, zip3, zip4, ..., and liftM,
liftM2, ...?
Each of them has a type that fits into a pattern, mainly the
On Jun 26, 2010, at 4:33 AM, Andrew Coppin wrote:
It's a bit like trying to learn Prolog from somebody who thinks that
the difference between first-order and second-order logic is somehow
common knowledge.
A first order logic quantifies over values, and a second order logic
quantifies
Alexander Solla wrote:
On Jun 26, 2010, at 4:33 AM, Andrew Coppin wrote:
It's a bit like trying to learn Prolog from somebody who thinks that
the difference between first-order and second-order logic is somehow
common knowledge.
A first order logic quantifies over values, and a second
Brandon S Allbery KF8NH wrote:
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
On 6/26/10 07:28 , Andrew Coppin wrote:
Oh, right. So you mean that as well as being able to say Foo Bar, you can
say Foo 7, where 7 is (of course) a value rather than a type. (?)
A bit more than that:
On Sat, Jun 26, 2010 at 11:23 AM, Andrew Coppin andrewcop...@btinternet.com
wrote:
Brandon S Allbery KF8NH wrote:
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
On 6/26/10 07:28 , Andrew Coppin wrote:
Oh, right. So you mean that as well as being able to say Foo Bar, you
can
say Foo 7,
On Jun 26, 2010, at 11:21 AM, Andrew Coppin wrote:
A first order logic quantifies over values, and a second order
logic quantifies over values and sets of values (i.e., types,
predicates, etc). The latter lets you express things like For
every property P, P x. Notice that this
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
On 6/26/10 14:58 , Jason Dagit wrote:
On Sat, Jun 26, 2010 at 11:23 AM, Andrew Coppin andrewcop...@btinternet.com
mailto:andrewcop...@btinternet.com wrote:
Brandon S Allbery KF8NH wrote:
A bit more than that: imagine now that you can
Andrew Coppin wrote:
Right, I see.
So is there a specific reason why Haskell isn't dependently typed then?
One problem with dependent types as I understand it is that type
inference is not guaranteed to terminate.
Erik
--
On Sat, Jun 26, 2010 at 6:55 PM, Erik de Castro Lopo
mle...@mega-nerd.com wrote:
One problem with dependent types as I understand it is that type
inference is not guaranteed to terminate.
Full type inference is undecidable in most interesting type systems
anyway. It's possible for the
Gregory Crosswhite wrote:
On 6/25/10 9:49 PM, wren ng thornton wrote:
[1] http://eclipse-clp.org/ is currently down, but can be accessed at
http://87.230.22.228/
[2] http://www.mercury.csse.unimelb.edu.au/
[3] http://www.lix.polytechnique.fr/~dale/lProlog/
[4]
Andrew Coppin wrote:
Stephen Tetley wrote:
On 26 June 2010 08:07, Andrew Coppin andrewcop...@btinternet.com wrote:
Out of curiosity, what the hell does dependently typed mean anyway?
How about:
The result type of a function may depend on the argument value
(rather than just the argument
Andrew Coppin wrote:
I think I looked at Coq (or was it Epigram?) and found it utterly
incomprehensible. Whoever wrote the document I was reading was obviously
very comfortable with advanced mathematical abstractions which I've
never even heard of.
One of the things I've found when dealing
I've noticed over the - okay, over the months - that some folks enjoy the
puzzle-like qualities of programming in the type system (poor Oleg, he's
become #haskell's answer to the Chuck Norris meme commonly encountered in
MMORPGs).
Anyway,... are there any languages out there whose term-level
On Fri, Jun 25, 2010 at 2:26 PM, Walt Rorie-Baety black.m...@gmail.comwrote:
I've noticed over the - okay, over the months - that some folks enjoy the
puzzle-like qualities of programming in the type system (poor Oleg, he's
become #haskell's answer to the Chuck Norris meme commonly encountered
Jason Dagit wrote:
On Fri, Jun 25, 2010 at 2:26 PM, Walt Rorie-Baety black.m...@gmail.comwrote:
I've noticed over the - okay, over the months - that some folks enjoy the
puzzle-like qualities of programming in the type system (poor Oleg, he's
become #haskell's answer to the Chuck Norris meme
Are any of those compatible with Haskell, so that we could mix code in
that language with Haskell code?
Cheers,
Greg
On 6/25/10 9:49 PM, wren ng thornton wrote:
Jason Dagit wrote:
On Fri, Jun 25, 2010 at 2:26 PM, Walt Rorie-Baety
black.m...@gmail.comwrote:
I've noticed over the - okay,
On Mon, 2009-03-30 at 20:54 +0100, Lennart Augustsson wrote:
I wasn't questioning the utility of John's library.
But I saw him mentioning unary numbers and I think it's a mistake to
use those for anything practical involving even moderately sized
numbers.
Also agreed! tfp supports rational
There is already a library for type level number, called typelevel.
It's nice because it uses decimal representation of numbers and can
handle numbers of reasonable size.
I use it in the LLVM bindings.
-- Lennart
On Mon, Mar 30, 2009 at 1:07 AM, spoon sp...@killersmurf.com wrote:
I've been
Hello,
I suppose Lennart is referring to type-level [1]. But type-level uses
functional dependencies, right?
There is also tfp [2], which uses type families. In general, how would you
say your work compares to these two?
Thanks,
Pedro
[1]
Lennart,
I think the major emphasis that John's library has is on doing things other
than numbers well in the type system, using the type family syntax to avoid
the proliferation of intermediary names that the fundep approach yields.
I think his type family approach for type-level monads for
Haskell not having 'polymorphic kinds'.
Is there a good description of why Haskell doesn't have polymorphic kinds?
2009/3/30 Edward Kmett ekm...@gmail.com
Lennart,
I think the major emphasis that John's library has is on doing things other
than numbers well in the type system, using the
John Van Enk wrote:
Haskell not having 'polymorphic kinds'.
Is there a good description of why Haskell doesn't have polymorphic kinds?
IANA expert but polymorphic kinds belong to a set of reasonably new
influences (e.g. from dependently typed programming languages and
generic
I suppose having a good description of what I'd like to do might help: I'd
like to be able to make an N-Tuple an instance of a type class.
class Foo a where
instance Foo (,) where
instance Foo (,,) where
The different kindedness of (,) and (,,) prevent this from
Thats a bit farther down the rabbit hole than the concern in question,
though certainly related.
An example of what you could write with polymorphic kinds, inventing a
notation for polymorphic kind variables using 'x to denote a polymorphic
kind x, which could subtitute in for a kind k = * | **
I wasn't questioning the utility of John's library.
But I saw him mentioning unary numbers and I think it's a mistake to
use those for anything practical involving even moderately sized
numbers.
I'd love to see a good type level programming library. There's a lot
of it out there, but it's never
On Mon, Mar 30, 2009 at 3:54 PM, Lennart Augustsson
lenn...@augustsson.netwrote:
I wasn't questioning the utility of John's library. But I saw him
mentioning unary numbers and I think it's a mistake to
use those for anything practical involving even moderately sized
numbers.
Completely
I suppose having a good description of what I'd like to do might help: I'd
like to be able to make an N-Tuple an instance of a type class.
class Foo a where
instance Foo (,) where
instance Foo (,,) where
The different kindedness of (,) and (,,) prevent this from working.
Not that this
I've been doing some basic work on a support library for type level
programming ( see
http://hackage.haskell.org/trac/summer-of-code/ticket/1541 ). I know
there have been similar attempts using fundeps ( Edward Kmett showed me
some of his work, but I've lost the address... ) but this approach
Aaron Denney wrote:
On 2008-09-27, Andrew Coppin [EMAIL PROTECTED] wrote:
Ah - so the Prolog programs as type signatures thing is *his* fault?! ;-)
No, he merely takes advantage of it.
Heh. OK. ;-)
By the way... I've seen a lot of type-level programs that allow you to
express
On 2008 Sep 28, at 4:47, Andrew Coppin wrote:
By the way... I've seen a lot of type-level programs that allow you
to express (and therefore verify) some pretty extreme properties of
your code. In other words, you can make the compiler do more
checking than it normally would. But the actual
Dear all,
Recently I was playing around with encoding matrices in the type-level
system. Thereby one can enable the multiplication of matrices. The general
idea (which can be read about at (
http://notvincenz.blogspot.com/2007/06/generalized-matrix-multiplication.html)
is that there is more
Hi,
I have a type class similar to this one.
data T
class Foo ns a b c | ns - a, ns - b, ns - c where
mkFoo :: ns
defaultA :: a
defaultB :: c - IO b
defaultC :: [T] - c
f :: c - b - a - (b, Int)
The idea is, that I define classes of components where the data types
of the
Thomas Schilling wrote:
data T
class Foo ns a b c | ns - a, ns - b, ns - c where
mkFoo :: ns
defaultA :: a
defaultB :: c - IO b
defaultC :: [T] - c
f :: c - b - a - (b, Int)
data DefaultA
instance Foo ns a b c = Apply DefaultA ns a where
apply _ _ =
Hi All,Inspired by Oleg's Eliminating Array Bound Checking through
Non-dependent types http://okmij.org/ftp/Haskell/types.html#branding,I am
attempting to write code that will receive an array from C land and convert
it to a type safe representation. The array could have n dimensions where n
55 matches
Mail list logo
