[Haskell-cafe] Re: Type-Level Naturals Like Prolog?

[Bulat Ziganshin]

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 at gmail.com