On Sep 2, 2006, at 2:01 PM, skaller wrote:
> On Sat, 2006-09-02 at 09:37 -0400, Peter Tanski wrote:
>>> No, the problem is I never defined
>>>
>>> <a,b,c>
>>>
>>> The <> here has 3 arguments. The 'obvious' definition is
>>>
>>> <f,g,h> (a,b,c) = (f a, g b, h c)
>>>
>>> which is what we want. Etc for 4, 5. I can easily
>>> define <> in the Felix *compiler*. There is no way to
>>> define it in *Felix*.
>>>
>>> You can't even write out its type.
>>
>> How will pattern calculus solve it?
>
> Recursive expansion of patterns n times for variable
> n allows them to match ANY tuple. The user can write
> the match, and reduction rules, straight into the
> library.
Ah. So in pattern calculus a Tuple will be defined similar to a List:
>> (This is a real question, not a
>> jibe.) Felix is unlike other functional languages in that the
>> operators have definite types
>
> I don't understand what you mean.
My personal head-banging came when trying to understand why the Felix
function 'pair' created a unified TYPE rather than a product: TYPE *
TYPE. After reading Cardelli's paper, I now understand that pair and
tuple are (or should be) distinct types: pair is the product type,
logically "AND," while tuple is the disjoint union type, logically "OR."
As for your understanding, either I am wrong or I am making different
distinctions than the standard way functional programmers talk about
things (likely the former). Here is the best explanation I can give
without introducing any of my own distinctions:
A Haskell "data" type is like a variant in OCaml
[Haskell]:
data Person = FirstName String
| LastName String
[OCaml]:
type person = FirstName of string | LastName of string ;;
At least in Haskell, a tuple has a formal "type" only in the sense
that it is a data type defined solely in terms of a constructor. For
example:
data (,,,) a b c = (,,,) a b c
There are, unfortunately, many "tuple" definitions like this, all the
way up to 62 in GHC.
Note that the definition is not:
data (,,,) a b c = (a,b,c)
or
data (,,,) a b c = a,b,c,()
Note also that the "name" of this data type is the constructor
itself. According to the Haskell98 standard the definition of a
tuple is a "value," not a singular "type," so particular
implementations may differ in their interpretation of how a tuple
operates. In the original Miranda language, tuples, like lists, were
special cases of data types (then called "structured" types) in that
they were built in. Note: if you refer to "Implementing Functional
Languages--A Tutorial," section 2.7 Mark 5, in Haskell only "data"
declarations are structured types--Haskell also has "records," as a
special case of "data" types; in "Subtyping Recursive Types,"
Cardelli refers to function types ( a -> b ) as "structured" types.
All this tuple "type" does is name the special tuple constructor for
the Haskell system to understand, so, for example, it will not give
you a type error if you improperly construct a tuple:
[ghci prompt]
--------------
Prelude> let a = (,,) 1 2 3
Prelude> a
(1,2,3)
Prelude> let b = (,,,) 1 2 3
Prelude> :type b
b :: forall d. d -> (Integer, Integer, Integer, d)
--------------
As you can see from the type of "b" above, there was no syntax error
and there was also a very odd response: there is an undefined
existential "d" sitting in the unfilled (last) part of the quadruple-
tuple. Since data constructors (like metatypes in Felix) are
essentially functions, if you apply a function with fewer arguments
than it calls for you get the standard currying response, which in
Haskell translates to a lambda expression that is essentially a new
function to carry the extra arguments:
--------------
Prelude> let add3 x y z = x + y + z
Prelude> :t add3
add3 :: forall a. (Num a) => a -> a -> a -> a
Prelude> let curriedAdd = add3 1 2
Prelude> :t curriedAdd
curriedAdd :: Integer -> Integer
--------------
(Here, the system simplifies 'curriedAdd' into the lambda expression
(\x -> (add3 1 2) x).)
If you attempt construct a _data_ type with fewer arguments than
required you will get a _type_ error. For example:
--------------
Prelude> let (zoe::Person) = FirstName
<interactive>:1:20:
Couldn't match `Person' against `t -> t1'
Expected type: Person
Inferred type: t -> t1
Expected type: Person
Inferred type: String -> Person
In a pattern binding: (zoe :: Person) = FirstName
--------------
(This is a type error: Person has a static type, but an incompletely
constructed person is essentially a lambda expression of type (t ->
t1). As you can see from the "Inferred type:" statement, the
'FirstName String' data constructor for type Person is really a
function type: FirstName :: String -> Person. Don't get confused
when I call a function type a separate type; it is really only a type
signature since in Haskell function closures represent lambda
abstractions. Since the application of the data constructor
FirstName to nothing resulted in a lambda expression (\s -> Person)
and not Person, we have a type error (between "Expected type" and
"Inferred Type." The end result (t1) would have been Person if I had
included a string after "FirstName.") In OCaml the error would be a
little clearer:
--------------
# let zoe = FirstName ;;
Characters 10-19:
let zoe = FirstName ;;
^^^^^^^^^
The constructor FirstName expects 1 argument(s),
but is here applied to 0 argument(s)
--------------
(I think this may be a system-supplied error, not necessarily a type
error.)
To get back to the point I was attempting to make, in the above
incorrectly-applied tuple example,
--------------
Prelude> let b = (,,,) 1 2 3
Prelude> :type b
b :: forall d. d -> (Integer, Integer, Integer, d)
--------------
GHCi did not report a type constructor error, instead it *inferred*
the value of the last place. This is not the behavior of a data
type, this is the behavior of a function and as you know functions
literally have the "type" of their arguments: ( f :: t1 -> t2 -> t3 )
--Haskell uses the (::) operator to denote "type" you saw this in the
example of (zoe :: Person), above. In other words, there is no tuple
"type," as a distinct type apart from its arguments and, in fact, b
above _is_ a lambda expression:
--------------
Prelude> let c = b 4 -- c = (Integer,Integer,Integer,d) 4
Prelude> :t c
c :: (Integer, Integer, Integer, Integer)
--------------
This behavior still follows the Haskell98 standard, pg. 22:
"(e1, ... , ek) for k >= 2 is an instance of a k-tuple as defined in
the Prelude, and requires no translation. If t1 through tk are the
types of e1 through ek, respectively then the type of the resulting
tuple is (t1, ... , tk)"
I was partly wrong--probably the source of your confusion: OCaml
seems to define a tuple as a cartesian product (a product-type).
To make another contrast, the empty set in OCaml and Felix is (),
which is the base type of the tuple type (unit). In Haskell ()
exists but it is a completely separate operator from tuple, and it
does not denote 'unit' (although that is one of its uses, especially
in the IO Monad) but 'bottom,' the logical termination operator we
all know and love: (_|_). (In Haskell this is a very important type
because it marks the termination point for many things, including
case matches and recursion--the base case. _|_ is how Haskell deals
with the problem of potentially infinite recursion.)
>> (in Haskell the tuple operator is not a
>> type but an operation;
>
> Still don't understand: Felix has both a tuple
> constructor AND a tuple type constructor.
I hope my above example might help explain. The tuple type
constructor in Haskell is only a way for the Haskell language have a
name for the primitive operation (function, really) of the tuple
constructor; otherwise the result of applying this tuple type
constructor is not a particular "(,,,)" data type but the special
construction containing the types of its arguments. In OCaml the
literal type of a tuple is the product of its elements:
--------------
# let tup = (1,2,3) ;;
val tup : int * int * int = (1, 2, 3)
--------------
which still does not seem like a separate type in the same sense that
a list is a separate type (in Haskell a list of chars has type
[Char]); in OCaml a tuple is examined as a complete product but that
product type always seems to be described in terms of its elements.
For example:
--------------
# let tup = (1,2,3) ;;
val tup : int * int * int = (1, 2, 3)
# let f (x:int) (y:int) (z:string) = (x,y,z);;
val f : int -> int -> string -> int * int * string = <fun>
# f tup ;;
Characters 2-5:
f tup ;;
^^^
This expression has type int * int * int but is here used with type int
--------------
(The error message here is actually matching each type of the tuple
and fails to match the last 'int' against the last 'string' expected
by fun f's type.)
I hope all these examples weren't pedantic. Maybe you already have
the correct concept named in your head as you read this, but at least
you understand why the unified TYPE resulting from pair : TYPE * TYPE
-> TYPE is unusual.
> There's just no way to write functions which operate on
> bound terms: the macro processor CAN do it already, for
> untyped unbound terms (but you lose lexical scoping etc:
> macro processing sucks :)
That's exactly what template meta-programming does: it gives the
programmer special access to values the compiler sees. Meta-
programming may not be necessary: I am not sure it can't be done
using Felix's axioms and reductions.
> Unfortunately, the Felix type system
> supports type functions and products:
>
> c | -> | *
>
> but not sums, so I don't have many constructors to play
> with other than constants like 'int' :)
You mean, Felix does not have the "disjoint union" type "+"? Tuples
should properly be disjoint unions. Now there's something to work on.
> So actually if someone could read the paper and help
> me understand if the implementation is right .. that
> would help! Reading my Ocaml code is not a thing
> to look forward to (but I can explain what some
> of it does .. :)
In case you couldn't already tell, I am working through Cardelli's
paper. I will be gone tomorrow but I will find some time to squeeze
in after that.
-Pete
-------------------------------------------------------------------------
Using Tomcat but need to do more? Need to support web services, security?
Get stuff done quickly with pre-integrated technology to make your job easier
Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronimo
http://sel.as-us.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642
_______________________________________________
Felix-language mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/felix-language
