Thank you to everyone for the responses. I guess what I should have clarified is that I know how Peano numbers are *normally* encoded in the type language (I am very familiar with the HList library), but I would like to know why the type language appears to require data structures to do so while [Idealised] Prolog has none. Niklas Broberg helpfully corrected my Prolog:
That is not a valid encoding of peano numbers in prolog, so I think that's where your problems stem from. :-)
% defining natural numbers natural(zero). natural(s(X)) :- natural(X).
% translate to integers toInt(zero, 0). toInt(s(X), N) :- toInt(X, Y), N is Y + 1.
Thank you. I can now more precisely state that what I'm trying to figure out is: what is 's', a predicate or a data structure? If it's a predicate, where are its instances? If not, what is the difference between the type language and Prolog such that the type language requires data structures?
jawarren:
Thank you to everyone for the responses. I guess what I should have clarified is that I know how Peano numbers are *normally* encoded in the type language (I am very familiar with the HList library), but I would like to know why the type language appears to require data structures to do so while [Idealised] Prolog has none.
Niklas Broberg helpfully corrected my Prolog:
That is not a valid encoding of peano numbers in prolog, so I think that's where your problems stem from. :-)
% defining natural numbers natural(zero). natural(s(X)) :- natural(X).
% translate to integers toInt(zero, 0). toInt(s(X), N) :- toInt(X, Y), N is Y + 1.
Thank you. I can now more precisely state that what I'm trying to figure out is: what is 's', a predicate or a data structure? If it's a predicate, where are its instances? If not, what is the difference between the type language and Prolog such that the type language requires data structures?
It shouldn't actually require new data structures, just new types (with no inhabiting values). such as, data Zero data Succ a So there are no values of this type (other than bottom). That is, you can just see 'data' here as a way of producing new types to play with in the type checker. -- Don
Hello Jared, Tuesday, July 18, 2006, 9:05:09 AM, you wrote:
% defining natural numbers natural(zero). natural(s(X)) :- natural(X).
% translate to integers toInt(zero, 0). toInt(s(X), N) :- toInt(X, Y), N is Y + 1.
Thank you. I can now more precisely state that what I'm trying to figure out is: what is 's', a predicate or a data structure? If it's a predicate, where are its instances? If not, what is the difference between the type language and Prolog such that the type language requires data structures?
it's data structure, to be exact, it's data constructor - just like, for example, "Just" in Haskell. Haskell requires that all data constructors should be explicitly defined before they can be used. you can use "Just" to construct data values only if your program declares "Just" as data constructor with "data" definition like this: data Maybe a = Just a | Nothing Prolog is more liberate language and there you can use any data constructors without their explicit declarations, moreover, there is no such declarations anyway The more important difference is what Prolog is _logic_ programming language and there you can use unification and backtracking in functions' definitions. Haskell is _not_ logic programming language so you can't define functions what use these techniques. The humor, though, is that Haskell's multi-parameter type classes defines logic programming language, but at the _type_ level. Values of this language is _types_ instead of ordinary values. And naturally, instead of data constructors - _type_ constructors are used to construct new type values and in the unification operations. So, you can't use "Just" in this language, but "Maybe" can be used. GHC also supports nullary data definitions which defines just type constructor without data constructors: data Zero data Succ a i once said you about good paper on type-classes level programming. if you want, i can send you my unfinished article on this topic which shows correspondences between logic programming, type classes and GADTs -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
% defining natural numbers natural(zero). natural(s(X)) :- natural(X).
% translate to integers toInt(zero, 0). toInt(s(X), N) :- toInt(X, Y), N is Y + 1.
Thank you. I can now more precisely state that what I'm trying to figure out is: what is 's', a predicate or a data structure? If it's a predicate, where are its instances? If not, what is the difference between the type language and Prolog such that the type language requires data structures?
it's data structure, to be exact, it's data constructor - just like, for example, "Just" in Haskell. Haskell requires that all data constructors should be explicitly defined before they can be used. you can use "Just" to construct data values only if your program declares "Just" as data constructor with "data" definition like this:
data Maybe a = Just a | Nothing
Prolog is more liberate language and there you can use any data constructors without their explicit declarations, moreover, there is no such declarations anyway
[deletia]
i once said you about good paper on type-classes level programming. if you want, i can send you my unfinished article on this topic which shows correspondences between logic programming, type classes and GADTs
So predicates and data constructors have similar syntax but different semantics in Prolog? Say, for the sake of argument, if I wanted to do automatic translation, how would I tell which was which in a Prolog program? "Faking it: Simulating dependent types in Haskell" certainly explains *one* way to simulate dependent types, but I need to justify the existence of type constructors in an Idealised Haskell, so I must understand why the implementation in Prolog does not appear to be a literal translation. I would love to read your article! (I can give you a [forthcoming?] citation if I ever get through this part of my thesis. :-/)
Hello Jared, Tuesday, July 18, 2006, 11:12:09 PM, you wrote:
% defining natural numbers natural(zero). natural(s(X)) :- natural(X).
% translate to integers toInt(zero, 0). toInt(s(X), N) :- toInt(X, Y), N is Y + 1.
Thank you. I can now more precisely state that what I'm trying to figure out is: what is 's', a predicate or a data structure? If it's a predicate, where are its instances? If not, what is the difference between the type language and Prolog such that the type language requires data structures?
it's data structure, to be exact, it's data constructor - just like, for example, "Just" in Haskell. Haskell requires that all data constructors should be explicitly defined before they can be used. you can use "Just" to construct data values only if your program declares "Just" as data constructor with "data" definition like this:
data Maybe a = Just a | Nothing
Prolog is more liberate language and there you can use any data constructors without their explicit declarations, moreover, there is no such declarations anyway
[deletia]
i once said you about good paper on type-classes level programming. if you want, i can send you my unfinished article on this topic which shows correspondences between logic programming, type classes and GADTs
So predicates and data constructors have similar syntax but different semantics in Prolog? Say, for the sake of argument, if I wanted to do automatic translation, how would I tell which was which in a Prolog program?
how about buying some little Prolog book? :) prolog statements look as phrase :- phrase, phrase, phrase. where each phrase has syntax predicate(data,data,data) where data has one of the following shapes simple or data(data,data,data) where simple may be constant (any lower-cased word) or represent variable (upper-cased word or _) Prolog constants plays the same role as Haskell data constructors - they can be lowest-level data items or a way to construct something more complex from simpler things. for example, Haskell value "Right (Nothing, Just Nothing)" can be translated to Prolog value "right (nothing, just (nothing))" next, Prolog is untyped language. ALL the values belongs to one common datatype. there is no type declarations, any value can be constructed by rules i given for 'data' (of course, you should not use variables, only constants). if you construct 'data' using both variables and constants - you get the pattern to match in predicates.
"Faking it: Simulating dependent types in Haskell" certainly explains *one* way to simulate dependent types, but I need to justify the existence of type constructors in an Idealised Haskell, so I must understand why the implementation in Prolog does not appear to be a literal translation.
Haskell, unlike Prolog, has strict static typing. each value and each variable has its type. these types are declared via 'data' statements: data Typename = Constructor1 Subtype11 Subtype12 | Constructor2 Subtype21 Subtype22 these statements defines correspondence between types and values - using 'data' declarations, we can find for each value exact type to which it belongs. for example, value "(LT, Just True)" has the type "(Ordering, Maybe Bool)", what you can discover by finding 'data' declarations where each of used data constructor (LT, Just, True) is defined Haskell supports logic programming on type constructors (which are defined on the left side of 'data' statement), not on the data constructors (defined at the right side), but the requirement remains - type constructors with which 'instance' definitions deal, should be predefined in program, you can't use type constructors not defined in some 'data' statements. because in this case you don't use data constructors (i.e., the right side), you can use nullary types for this purpose: data Zero data Succ a is that, theoretically, possible to change Haskell so that it can use any type constructors in instance declarations without predeclaring them in 'data' statements? yes, that's possible. the only information Haskell receives from these 'data' statements is type constructor arity and if Haskell compiler will have another way to guess what is arity - data statements can be avoided -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
On Tue, 18 Jul 2006, Jared Warren wrote:
% defining natural numbers natural(zero). natural(s(X)) :- natural(X).
% translate to integers toInt(zero, 0). toInt(s(X), N) :- toInt(X, Y), N is Y + 1.
Thank you. I can now more precisely state that what I'm trying to figure out is: what is 's', a predicate or a data structure? If it's a predicate, where are its instances? If not, what is the difference between the type language and Prolog such that the type language requires data structures?
it's data structure, to be exact, it's data constructor - just like, for example, "Just" in Haskell. Haskell requires that all data constructors should be explicitly defined before they can be used. you can use "Just" to construct data values only if your program declares "Just" as data constructor with "data" definition like this:
data Maybe a = Just a | Nothing
Prolog is more liberate language and there you can use any data constructors without their explicit declarations, moreover, there is no such declarations anyway
[deletia]
i once said you about good paper on type-classes level programming. if you want, i can send you my unfinished article on this topic which shows correspondences between logic programming, type classes and GADTs
So predicates and data constructors have similar syntax but different semantics in Prolog?
That is right. The syntax and naming are different from Haskell though. They are called respectively predicate and function symbols/functors, and written like f(x1,...,xn) rather than F x1 ... xn. Terms are made of possibly nested function symbols and variables, e.g. f(f(f(a,X))) where f and a are used as function symbols Atoms are made of a predicate symbol and terms,e.g. p(f(f(f(a,X)))) where p is used as a predicate symbol f and a are used as function symbols Note that the same name can be used with multiple argument numbers and both as a predicate and a function symbol.
Say, for the sake of argument, if I wanted to do automatic translation, how would I tell which was which in a Prolog program?
Based on the syntax. Basically the top-level symbols are predicate symbols and the nested ones are function symbols, e.g. in a clause p(f(X)) :- q(h(i)), j(k) = l(m). p, q and '=' are predicate symbols and all the rest are function symbols. It's probably good to read a bit about it in a proper reference. Wikipedia's Prolog entry lists a number of tutorials. Cheers, Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be
participants (4)
-
Bulat Ziganshin -
dons＠cse.unsw.edu.au -
Jared Warren -
Tom Schrijvers