[Haskell-beginners] Re: dependent types

pat browne Patrick.Browne at comp.dit.ie
Mon Jul 20 17:18:15 EDT 2009


Maurí­cio,
Thanks for your rapid feedback, I will study your code.

>> I think (but someone with better knowledge) the term "dependent
>> type" means something else:
>> http://en.wikipedia.org/wiki/Dependent_types

>From your first link I think the term *dependent type* is defined as a
type that depends on *values* of other types. The semantic that I am
trying to express is that one type depends on another type.
Specifically, the type of a name depends on the type of the object. For
example a Person with a Name would give a Persons-Name and a Dog with a
Name would give a Dogs-Name. The paper [1] describe several styles of
dependency
     Types depending on values called dependent types
     Types depending on types called parametric and type-indexed types

[1]Comparing Approaches to Generic Programming Haskell by Hinze,
Jeuring, and LÄoh

Best regards,
Pat


Maurí­cio wrote:
>> The intended semantics are:
>>     Two objects are equal if they have the same name.
>>     The type of the name depends on the type of the object
> 
>> 3) How would I write an instance of Named that implements the name
>> function correctly.
> 
> I think (but someone with better knowledge) the term "dependent
> type" means something else:
> 
> http://en.wikipedia.org/wiki/Dependent_types
> 
> I'm sure you'll be interested in type families, which offer a
> better and richer syntax to what you want:
> 
> http://www.haskell.org/ghc/docs/latest/html/users_guide/type-families.html
> 
> I tried rewriting your example using ghc-6.8.2 but I wasn't
> able to build it, and since ghc-6.8.* isn't actually supposed
> to properly support type families I though I could give you a
> bad example even if I get it to build :) So I'm leaving it here
> just in case someone wants to use it as a base:
> 
> ------
> module Main (main) where
> 
> data (Eq a) => Object a = Object a
> 
> class (Eq (NameType o)) => Named o where
>   type NameType o :: *
>   name :: o -> NameType o
>   equals :: o -> o -> Bool
>   equals o1 o2 = (name o1) == (name o2)
> 
> instance (Named a) => Eq a where
>   (==) = equals
> 
> instance Named (Object Integer) where
>   type NameType (Object Integer) = Integer
>   name (Object i) = i
> 
> f,g :: Object Integer
> f = Object 1
> g = Object 2
> 
> main = putStrLn $ show $ f == g
> ------
> 
> Best,
> Maurício
> 
> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org
> http://www.haskell.org/mailman/listinfo/beginners




More information about the Beginners mailing list