[Haskell] PhD position in dependent types/functional programming at Chalmers

[Andreas Abel]

We have an opening for a PhD student in dependent type theory and
functional programming at Chalmers. Here is an excerpt from the ad:

  The PhD student will join the Programming Logic group and contribute
  to its research on dependent type theory and functional programming.
  Topics of interest include the following directions of work:

  - Design of dependently typed functional programming languages.

  - Theory and implementation of type checkers, compilers etc. for
dependently typed functional programming languages.

  - Investigations into the use of dependently typed functional
programming languages, both as programming languages and as logical
systems.

  - Models and applications of (homotopy) type theory.

Note that work on and in Agda matches several of the topics above.

Full text of the advertisement:

  http://www.chalmers.se/en/about-chalmers/vacancies/?rmpage=jobrmjob=2902

Application deadline:

  March 31, 2015

--
Andreas AbelDu bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.a...@gu.se
http://www2.tcs.ifi.lmu.de/~abel/

___
Haskell mailing list
Haskell@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell

[Haskell] PhD Position in dependent types, testing hardware design

[Wouter Swierstra]

==
VACANCY : 1x Phd position in dependent types, testing  hardware design
==

The research group of Software Technology is part of the Software
Systems division of in the department of Information and Computer
Science at the Utrecht University. We focus our research on functional
programming, compiler construction, program analysis, validation, and
verification.

Financed by the Netherlands Organisation for Scientific Research
(NWO), we currently have a job opening for:

* 1x PhD researcher (PhD student) Software Technology

The aim of the project is to develop a domain specific language for
testing and verifying hardware, embedded in a general purpose
dependently typed programming language.

Besides research, the successful candidate will be expected to help
supervise MSc students and assist teaching courses.

We aim to start September 1, 2014 at the latest, but preferably
sooner.

-
What we are looking for
-

The candidate should have an MSc in Computer Science, be highly
motivated, speak and write English well, and be proficient in
producing scientific reports. Knowledge of and experience with at
least one of the following four areas is essential:

 * functional programming, such as Haskell or ML;
 * dependently typed programming, such as Agda, Coq, or Idris;
 * software testing, including familiarity with libraries such as
   QuickCheck and SmallCheck;
 * hardware description languages, such as Lava or VHDL;

-
What we offer
-

The candidate is offered a full-time position for four years. A
part-time of at least 0.8 fte may also be possible. The salary is
supplemented with a holiday bonus of 8% and an end-of-year bonus of
8,3% per year. In addition we offer: a pension scheme, a partially
paid parental leave, flexible employment conditions. Conditions are
based on the Collective Labour Agreement Dutch Universities. The
research group will provide the candidate with necessary support on
all aspects of the project. More information is available on the
website:

  Terms and employment: http://bit.ly/1elqpM7

A part-time of at least 0.8 fte may also be possible. Salary starts
at EURO 2,083 and increases to EURO 2,664 gross per month in the fourth
year of the appointment.

Utrecht is a great place to live, having been ranked as one of the
happiest places in the world, according to BBC travel.

  Living in Utrecht: http://bitly.com/HdbL0X

-
In order to apply
-

To apply please attach a letter of motivation, a curriculum vitae, and
(email) addresses of two referees. Make sure to also include a
transcript of the courses you have followed (at bachelor and master
level), with the grades you obtained, and to include a sample of your
scientific writing, such as your master thesis.

It is possible to apply for this position if you are close to
obtaining your Master's. In that case include a letter of your
supervisor with an estimate of your progress, and do not forget to
include at least a sample of your technical writing skills.

Application closes on the May 30th, 2014. You can apply through
the University's website:

  
http://ssl1.peoplexs.com/Peoplexs22/CandidatesPortalNoLogin/Vacancy.cfm?PortalID=4124VacatureID=654004

---
Contact
---

For further information you can direct your inquiries to:

Wouter Swierstra
phone: +31 (0)30 253 9207
e-mail: w.s.swiers...@uu.nl.
website: http://www.staff.science.uu.nl/~swier004
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [GHC] #5978: Type error in one function causes wrong type error report in another function in the presence of functionally dependent types

[GHC]

#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
--+-
  Reporter:  Lemming  |  Owner:  
  Type:  bug  | Status:  closed  
  Priority:  low  |  Milestone:  7.6.1   
 Component:  Compiler (Type checker)  |Version:  7.4.1   
Resolution:  fixed|   Keywords:  
Os:  Unknown/Multiple |   Architecture:  Unknown/Multiple
   Failure:  GHC rejects valid program| Difficulty:  Unknown 
  Testcase:  typecheck/should_fail/T5978  |  Blockedby:  
  Blocking:   |Related:  
--+-
Changes (by simonpj):

  * status:  new = closed
  * testcase:  = typecheck/should_fail/T5978
  * resolution:  = fixed


Comment:

 Recent changes in the type inference engine mean that you now get just one
 error, and on `monoBar`. To be honest I'm not 100% certain of why this has
 come right, and that means I'm not certain that the solution is robust
 (mabye it's a fluke).  But I'm sort of time, so I'm closing the ticket.
 But I'm adding the test as a regression test so we'll know immediately if
 it stops working.

 Thanks for the example.

 Simon

-- 
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/5978#comment:12
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Re: [GHC] #5978: Type error in one function causes wrong type error report in another function in the presence of functionally dependent types

[GHC]

#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
+---
Reporter:  Lemming  |   Owner:  
 
Type:  bug  |  Status:  new 
 
Priority:  low  |   Milestone:  7.6.1   
 
   Component:  Compiler (Type checker)  | Version:  7.4.1   
 
Keywords:   |  Os:  Unknown/Multiple
 
Architecture:  Unknown/Multiple | Failure:  GHC rejects valid 
program
  Difficulty:  Unknown  |Testcase:  
 
   Blockedby:   |Blocking:  
 
 Related:   |  
+---
Changes (by pcapriotti):

  * priority:  normal = low
  * milestone:  = 7.6.1


-- 
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/5978#comment:11
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Re: [GHC] #5978: Type error in one function causes wrong type error report in another function in the presence of functionally dependent types

[GHC]

#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
+---
Reporter:  Lemming  |   Owner:  
 
Type:  bug  |  Status:  new 
 
Priority:  normal   |   Milestone:  
 
   Component:  Compiler (Type checker)  | Version:  7.4.1   
 
Keywords:   |  Os:  Unknown/Multiple
 
Architecture:  Unknown/Multiple | Failure:  GHC rejects valid 
program
  Difficulty:  Unknown  |Testcase:  
 
   Blockedby:   |Blocking:  
 
 Related:   |  
+---

Comment(by Lemming):

 Replying to [comment:9 Lemming]:
  Now I got the same problem with type families and without functional
 dependencies.

 I have opened a new ticket for the issue with type families: #7010.

-- 
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/5978#comment:10
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Re: [GHC] #5978: Type error in one function causes wrong type error report in another function in the presence of functionally dependent types

[GHC]

#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
+---
Reporter:  Lemming  |   Owner:  
 
Type:  bug  |  Status:  new 
 
Priority:  normal   |   Milestone:  
 
   Component:  Compiler (Type checker)  | Version:  7.4.1   
 
Keywords:   |  Os:  Unknown/Multiple
 
Architecture:  Unknown/Multiple | Failure:  GHC rejects valid 
program
  Difficulty:  Unknown  |Testcase:  
 
   Blockedby:   |Blocking:  
 
 Related:   |  
+---

Comment(by Lemming):

 Now I got the same problem with type families and without functional
 dependencies.

-- 
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/5978#comment:9
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Re: [GHC] #5978: Type error in one function causes wrong type error report in another function in the presence of functionally dependent types

[GHC]

#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
+---
Reporter:  Lemming  |   Owner:  
 
Type:  bug  |  Status:  new 
 
Priority:  normal   |   Milestone:  
 
   Component:  Compiler (Type checker)  | Version:  7.4.1   
 
Keywords:   |  Os:  Unknown/Multiple
 
Architecture:  Unknown/Multiple | Failure:  GHC rejects valid 
program
  Difficulty:  Unknown  |Testcase:  
 
   Blockedby:   |Blocking:  
 
 Related:   |  
+---

Comment(by Lemming):

 Replying to [comment:5 simonpj]:

  I would certainly give type families a try, yes.  I'd be interested to
 hear how it goes.

 I have converted some of my code to type families. Unfortunately, since I
 depend on the llvm package, the code is now quite inconsistent, because
 llvm uses a lot of functional dependencies and it uses in turn the type-
 level package that requires even more functional dependencies. Thus for
 now I cannot get rid of the problematic code. My hope is that we can
 remove all of these functional dependencies when the type level naturals
 (#4385) become part of GHC HEAD.

-- 
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/5978#comment:6
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Re: [GHC] #5978: Type error in one function causes wrong type error report in another function in the presence of functionally dependent types

[GHC]

#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
+---
Reporter:  Lemming  |   Owner:  
 
Type:  bug  |  Status:  new 
 
Priority:  normal   |   Milestone:  
 
   Component:  Compiler (Type checker)  | Version:  7.4.1   
 
Keywords:   |  Os:  Unknown/Multiple
 
Architecture:  Unknown/Multiple | Failure:  GHC rejects valid 
program
  Difficulty:  Unknown  |Testcase:  
 
   Blockedby:   |Blocking:  
 
 Related:   |  
+---

Comment(by simonpj):

 OK. So the error message is a bit odd.  Could be fixed, with some work.
 But as I undrestand it, this ticket is not standing in anyone's path.
 It's just a nice to have possible improvement, right?

-- 
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/5978#comment:7
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Re: [GHC] #5978: Type error in one function causes wrong type error report in another function in the presence of functionally dependent types

[GHC]

#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
+---
Reporter:  Lemming  |   Owner:  
 
Type:  bug  |  Status:  new 
 
Priority:  normal   |   Milestone:  
 
   Component:  Compiler (Type checker)  | Version:  7.4.1   
 
Keywords:   |  Os:  Unknown/Multiple
 
Architecture:  Unknown/Multiple | Failure:  GHC rejects valid 
program
  Difficulty:  Unknown  |Testcase:  
 
   Blockedby:   |Blocking:  
 
 Related:   |  
+---

Comment(by Lemming):

 At first I thought that the type checker is wrong, since it reports a type
 error where no type error is. If I understand you correctly, then GHC
 still correctly identifies type correct and type incorrect programs, only
 the error message is misleading. If so, then this bug has no high priority
 for me.
 You may simply add if this type error message confuses you, then better
 switch to type families to every type error message concerning functional
 dependencies. :-)

-- 
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/5978#comment:8
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Re: [GHC] #5978: Type error in one function causes wrong type error report in another function in the presence of functionally dependent types

[GHC]

#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
+---
Reporter:  Lemming  |   Owner:  
 
Type:  bug  |  Status:  new 
 
Priority:  normal   |   Milestone:  
 
   Component:  Compiler (Type checker)  | Version:  7.4.1   
 
Keywords:   |  Os:  Unknown/Multiple
 
Architecture:  Unknown/Multiple | Failure:  GHC rejects valid 
program
  Difficulty:  Unknown  |Testcase:  
 
   Blockedby:   |Blocking:  
 
 Related:   |  
+---

Comment(by Lemming):

 Sorry ... monoFoo is correct and monoBar is incorrect.
 But when I compile that module GHC reports two type errors: One for
 monoFoo and one for monoBar.
 If I remove monoBar, then monoFoo is accepted by GHC.

 The result of monoBar is Double, thus fromB=Double.
 The argument of polyBar in monoBar is of type Float, thus fromA=Float.
 From the functional dependencies it follows toB=Bool and toA=Char.
 Thus id would need type Char - Bool, which is a type error and this one
 is correctly spotted by GHC.
 But additionally also a type error for monoBar is reported, although
 monoBar is correct.
 It has type Float and it follows to=Char, but the 'to' type is not used in
 monoBar.

-- 
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/5978#comment:2
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Re: [GHC] #5978: Type error in one function causes wrong type error report in another function in the presence of functionally dependent types

[GHC]

#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
+---
Reporter:  Lemming  |   Owner:  
 
Type:  bug  |  Status:  new 
 
Priority:  normal   |   Milestone:  
 
   Component:  Compiler (Type checker)  | Version:  7.4.1   
 
Keywords:   |  Os:  Unknown/Multiple
 
Architecture:  Unknown/Multiple | Failure:  GHC rejects valid 
program
  Difficulty:  Unknown  |Testcase:  
 
   Blockedby:   |Blocking:  
 
 Related:   |  
+---
Changes (by simonpj):

 * cc: dimitris@… (added)


Comment:

 OK I see what is happening.  From the two definitions we get these
 wanted constraints:
 {{{
 monoFoo:   mf1: C Float alpha

 monoBar:   mb1: C Float beta,
mb2: C Double beta
 }}}
 where `alpha` and `beta` are otherwise-unconstrained unification
 variables.

 Now if we first do fundeps wrt the `instance` decls, we get `alpha = Char`
 from `mf1`, `beta = Char` from `mb1` and `beta = Bool` from `mb2`, the
 latter two yield an error.

 But if we first do fundeps ''between'' the wanted constraints, we get
 `alpha = beta`, so that leaves us with `(mf1: C Float alpha, mb2: C Double
 alpha)`.  Now we can solve `mb2` via the fundep with the `instance` to
 give `alpha=Bool`, and that leaves an error for the innocent `mf1`!

 Even this isn't quite what happens.  Functional dependencies are a pain.

 Simon

-- 
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/5978#comment:3
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Re: [GHC] #5978: Type error in one function causes wrong type error report in another function in the presence of functionally dependent types

[GHC]

#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
+---
Reporter:  Lemming  |   Owner:  
 
Type:  bug  |  Status:  new 
 
Priority:  normal   |   Milestone:  
 
   Component:  Compiler (Type checker)  | Version:  7.4.1   
 
Keywords:   |  Os:  Unknown/Multiple
 
Architecture:  Unknown/Multiple | Failure:  GHC rejects valid 
program
  Difficulty:  Unknown  |Testcase:  
 
   Blockedby:   |Blocking:  
 
 Related:   |  
+---

Comment(by Lemming):

 Would you suggest that I convert my code to type families?

-- 
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/5978#comment:4
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Re: [GHC] #5978: Type error in one function causes wrong type error report in another function in the presence of functionally dependent types

[GHC]

#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
+---
Reporter:  Lemming  |   Owner:  
 
Type:  bug  |  Status:  new 
 
Priority:  normal   |   Milestone:  
 
   Component:  Compiler (Type checker)  | Version:  7.4.1   
 
Keywords:   |  Os:  Unknown/Multiple
 
Architecture:  Unknown/Multiple | Failure:  GHC rejects valid 
program
  Difficulty:  Unknown  |Testcase:  
 
   Blockedby:   |Blocking:  
 
 Related:   |  
+---

Comment(by simonpj):

 I would certainly give type families a try, yes.  I'd be interested to
 hear how it goes.

-- 
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/5978#comment:5
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

[GHC] #5978: Type error in one function causes wrong type error report in another function in the presence of functionally dependent types

[GHC]

#5978: Type error in one function causes wrong type error report in another
function in the presence of functionally dependent types
---+
 Reporter:  Lemming|  Owner:
 
 Type:  bug| Status:  new   
 
 Priority:  normal |  Component:  Compiler (Type 
checker)
  Version:  7.4.1  |   Keywords:
 
   Os:  Unknown/Multiple   |   Architecture:  Unknown/Multiple  
 
  Failure:  GHC rejects valid program  |   Testcase:
 
Blockedby: |   Blocking:
 
  Related: |  
---+
 When trying to reduce my problem in #5970 to a simple program I
 encountered an even more obvious bug. The problem is essentially as
 follows: I have
 {{{
 correct :: T
 correct = ...

 wrong :: T
 wrong = f correct
 }}}
 where 'wrong' has a type error and 'correct' is type correct. If I
 outcomment 'wrong' then GHC correctly confirms type-correctness of
 'correct', but if 'wrong' is enabled then GHC claims a type error in both
 'wrong' and 'correct'.
 To me it looks like the type-checker is trying to unify types across
 function boundaries. This would explain both non-linear growth of type-
 checking time and the observed effect of incorrect type errors.
 See attached program for a working example.

-- 
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/5978
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

[Haskell-cafe] Type class for sequences with dependent types

[Robbert Krebbers]

Hello,

in a Haskell development I have to represent paths that have elements of 
alternating types. GADTs allow me to do this easily:


data AltList :: * - * - * where
  Nil   :: AltList a a
  ICons :: Int - AltList Int b - AltList () b
  UCons :: () - AltList () b - AltList Int b

Since I have various kinds of these data structures I defined a type 
class for common operations on such data structures.


class DepSequence l where
  nil :: l a a
  app :: l a b - l b c - l a c

The instance for AltList is as follows:

instance DepSequence AltList where
  nil = Nil
  Nil   `app` k = k
  ICons i l `app` k = ICons i (l `app` k)
  UCons i l `app` k = UCons i (l `app` k)

This all works nicely, however, I also want ordinary lists to be an 
instance of this class too. I tried the following:


type IntListAlt a b = [Int]
instance DepSequence IntListAlt where
  nil = []
  app = (++)

But GHC does not like this, it yields:

  Type synonym `IntListAlt' should have 2 arguments, but has been
  given none In the instance declaration for `DepList IntListAlt'

The following alternative works, but it is quite ugly

newtype IntList a b = IntList { getList :: [Int] }
instance DepSequence IntList where
  nil = IntList []
  app l k = IntList (getList l ++ getList k)

and also does not give me a nil of type [Int] and an app of type [Int] 
- [Int] - [Int].


Does anyone know whether Haskell allows me to do this in a better way?

Best,

Robbert

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Type class for sequences with dependent types

[Markus Läll]

Hi

This has been discussed here[1] and here[2], and the answer is that
its not possible because of making type inference generally
impossible. It would be a useful feature though, and could be
implemented by requiring the user give additional type signatures to
help the inference algorithm out. But that is AFAIK not implemented
yet.

[1] http://www.haskell.org/pipermail/haskell-cafe/2011-July/093790.html
[2] http://comments.gmane.org/gmane.comp.lang.haskell.glasgow.user/21017

On Thu, Jan 5, 2012 at 3:12 PM, Robbert Krebbers
mailingli...@robbertkrebbers.nl wrote:
 Hello,

 in a Haskell development I have to represent paths that have elements of
 alternating types. GADTs allow me to do this easily:

 data AltList :: * - * - * where
  Nil   :: AltList a a
  ICons :: Int - AltList Int b - AltList () b
  UCons :: () - AltList () b - AltList Int b

 Since I have various kinds of these data structures I defined a type class
 for common operations on such data structures.

 class DepSequence l where
  nil :: l a a
  app :: l a b - l b c - l a c

 The instance for AltList is as follows:

 instance DepSequence AltList where
  nil = Nil
  Nil       `app` k = k
  ICons i l `app` k = ICons i (l `app` k)
  UCons i l `app` k = UCons i (l `app` k)

 This all works nicely, however, I also want ordinary lists to be an instance
 of this class too. I tried the following:

 type IntListAlt a b = [Int]
 instance DepSequence IntListAlt where
  nil = []
  app = (++)

 But GHC does not like this, it yields:

  Type synonym `IntListAlt' should have 2 arguments, but has been
  given none In the instance declaration for `DepList IntListAlt'

 The following alternative works, but it is quite ugly

 newtype IntList a b = IntList { getList :: [Int] }
 instance DepSequence IntList where
  nil     = IntList []
  app l k = IntList (getList l ++ getList k)

 and also does not give me a nil of type [Int] and an app of type [Int] -
 [Int] - [Int].

 Does anyone know whether Haskell allows me to do this in a better way?

 Best,

 Robbert

 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe



-- 
Markus Läll

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Type class for sequences with dependent types

[Eugene Kirpichov]

Will this help?

data List a b where
List :: [a] - List a a

05.01.2012, в 17:12, Robbert Krebbers mailingli...@robbertkrebbers.nl 
написал(а):

 Hello,
 
 in a Haskell development I have to represent paths that have elements of 
 alternating types. GADTs allow me to do this easily:
 
 data AltList :: * - * - * where
  Nil   :: AltList a a
  ICons :: Int - AltList Int b - AltList () b
  UCons :: () - AltList () b - AltList Int b
 
 Since I have various kinds of these data structures I defined a type class 
 for common operations on such data structures.
 
 class DepSequence l where
  nil :: l a a
  app :: l a b - l b c - l a c
 
 The instance for AltList is as follows:
 
 instance DepSequence AltList where
  nil = Nil
  Nil   `app` k = k
  ICons i l `app` k = ICons i (l `app` k)
  UCons i l `app` k = UCons i (l `app` k)
 
 This all works nicely, however, I also want ordinary lists to be an instance 
 of this class too. I tried the following:
 
 type IntListAlt a b = [Int]
 instance DepSequence IntListAlt where
  nil = []
  app = (++)
 
 But GHC does not like this, it yields:
 
  Type synonym `IntListAlt' should have 2 arguments, but has been
  given none In the instance declaration for `DepList IntListAlt'
 
 The following alternative works, but it is quite ugly
 
 newtype IntList a b = IntList { getList :: [Int] }
 instance DepSequence IntList where
  nil = IntList []
  app l k = IntList (getList l ++ getList k)
 
 and also does not give me a nil of type [Int] and an app of type [Int] - 
 [Int] - [Int].
 
 Does anyone know whether Haskell allows me to do this in a better way?
 
 Best,
 
 Robbert
 
 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Type class for sequences with dependent types

[Robbert Krebbers]

Hi Eugene,

with respect to typing your solution is a lot nicer since the type 
arguments are not just ignored. But apart from that it does not help too 
much in the below example, since it does not allow me to get rid of the 
additional constructor (List in your case, IntList in mine) and it still 
does not give an instance nil of type [a], so I cannot write things like 
[x] `app` nil.


Fortunately, in my actual development, I used another type than list, so 
I could just redefine the type in the way you proposed. Assuming the 
type was actually a redefinition of lists, it would look like:


data List_ a b where
  Nil  :: List_ a a
  Cons :: a - List_ a a - List_ a a

and then I created a type synonym for convenience.

type List a = List_ a a

However, (for example) showing that List is a Functor fails with a 
similar error.


instance Functor List where ...

The good thing is that I do not need such instances at the moment, so it 
solves my problem for the time being.


Thank you, and also Markus, for the replies,

Robbert

On 01/05/2012 03:04 PM, Eugene Kirpichov wrote:

Will this help?

data List a b where
 List :: [a] -  List a a

05.01.2012, в 17:12, Robbert Krebbersmailingli...@robbertkrebbers.nl  
написал(а):


Hello,

in a Haskell development I have to represent paths that have elements of 
alternating types. GADTs allow me to do this easily:

data AltList :: * -  * -  * where
  Nil   :: AltList a a
  ICons :: Int -  AltList Int b -  AltList () b
  UCons :: () -  AltList () b -  AltList Int b

Since I have various kinds of these data structures I defined a type class for 
common operations on such data structures.

class DepSequence l where
  nil :: l a a
  app :: l a b -  l b c -  l a c

The instance for AltList is as follows:

instance DepSequence AltList where
  nil = Nil
  Nil   `app` k = k
  ICons i l `app` k = ICons i (l `app` k)
  UCons i l `app` k = UCons i (l `app` k)

This all works nicely, however, I also want ordinary lists to be an instance of 
this class too. I tried the following:

type IntListAlt a b = [Int]
instance DepSequence IntListAlt where
  nil = []
  app = (++)

But GHC does not like this, it yields:

  Type synonym `IntListAlt' should have 2 arguments, but has been
  given none In the instance declaration for `DepList IntListAlt'

The following alternative works, but it is quite ugly

newtype IntList a b = IntList { getList :: [Int] }
instance DepSequence IntList where
  nil = IntList []
  app l k = IntList (getList l ++ getList k)

and also does not give me a nil of type [Int] and an app of type [Int] -  [Int] 
-  [Int].

Does anyone know whether Haskell allows me to do this in a better way?

Best,

Robbert

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Constructor discipline and dependent types.

[Patrick Browne]

Hi,
My understanding of the constructor discipline (CD) is that it is a
restriction on the form of an equation that guarantees that the equation
represents an executable function. The CD restricts the LHS of an
equation to consist of a function name, constructors, and variables.
Also there should be no new variables on the RHS.
So CD permits function to be defined and prohibits general assertions
which are more in the domain of a specification language.
Question 1: Is the above a reasonable understanding of CD?

Question 2: I have read that the lack of dependent types (DT) prevents
writing general assertions in Haskell. Is CD related to DT?  If so how
are they related?

Regards,
Pat

This message has been scanned for content and viruses by the DIT Information 
Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Constructor discipline and dependent types.

[Stephen Tetley]

On 17 July 2011 10:03, Patrick Browne patrick.bro...@dit.ie wrote:

 Question 1: Is the above a reasonable understanding of CD?

From a brief look, constructor discipline (CD) restricts left-hand
sides of equations to have no function calls themselves.

http://users.dsic.upv.es/~gvidal/german/pepm97/paper.pdf

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] urWeb, Haskell and dependent types ....

[Vasili I. Galchin]

Hello,

 Here is probably a good paper to get people up to speed on dependent
types (ironically written by two contributors to this mailing list??):
okmij.org/ftp/papers/lightweight-static-capabilities.pdf



Vasili
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] linear and dependent types

[Dan Doel]

On Saturday 19 February 2011 1:11:23 AM Vasili I. Galchin wrote:
  BTW I was thinking of http://www.ats.org when I asked this question.

Technically speaking, if one considers ATS to be dependently typed, then one 
might as well also consider GHC to be dependently typed (with the right 
extensions enabled). ATS would easily be a nicer language in that respect, 
though.

-- Dan

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] linear and dependent types

[Vasili I. Galchin]

Hello,

   Does Haskell currently have support for linear types and dependent
types? If so, is it necessary to specify a pragma to use and if so, what
is the pragma(s)?


Kind regards,

Vasili
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] linear and dependent types

[Don Stewart]

vigalchin:
Hello,
 
�� Does Haskell currently have support for linear types and dependent 
 types?

No.

-- Don 

P.S. :-)

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] linear and dependent types

[Bas van Dijk]

On 18 February 2011 20:04, Vasili I. Galchin vigalc...@gmail.com wrote:
    Does Haskell currently have support for linear types and dependent
 types? If so, is it necessary to specify a pragma to use and if so, what
 is the pragma(s)?

While Haskell doesn't have full dependent types, as found in say Agda,
it (or rather GHC) does have some extensions that allow you to get
many of the advantages of full dependent types.

You may want to check out the documentation of: multi parameter type
classes, functional dependencies, type families, higher ranked types,
generalized algebraic datatypes, scoped type variables, pfff... we
have so many toys! :-)

You may also want to read some of the papers mentioned in:

http://www.haskell.org/haskellwiki/Dependent_type#Dependent_types_in_Haskell_programming

Regards,

Bas

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] linear and dependent types

[Vasili I. Galchin]

Thanks Bas.

 BTW I was thinking of http://www.ats.org when I asked this question.

REgards, Vasili

On Fri, Feb 18, 2011 at 6:19 PM, Bas van Dijk v.dijk@gmail.com wrote:

 On 18 February 2011 20:04, Vasili I. Galchin vigalc...@gmail.com wrote:
 Does Haskell currently have support for linear types and dependent
  types? If so, is it necessary to specify a pragma to use and if so,
 what
  is the pragma(s)?

 While Haskell doesn't have full dependent types, as found in say Agda,
 it (or rather GHC) does have some extensions that allow you to get
 many of the advantages of full dependent types.

 You may want to check out the documentation of: multi parameter type
 classes, functional dependencies, type families, higher ranked types,
 generalized algebraic datatypes, scoped type variables, pfff... we
 have so many toys! :-)

 You may also want to read some of the papers mentioned in:


 http://www.haskell.org/haskellwiki/Dependent_type#Dependent_types_in_Haskell_programming

 Regards,

 Bas

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] linear and dependent types

[oleg]

There has been extensive discussion of whether Haskell has dependent
types, made larger by the fact that the definition of
dependently-typed languages is a bit fuzzy. On some accounts, type
functions or GADTs are sufficient for calling a language
dependently-typed, and Haskell got both features.

The situation is clearer with linear types. First of all, Haskell has
all facilities for statically ensuring the proper use of
resources. The simplest example is enforcing the locking protocol: a
lock can be acquired no more than once; only acquired locks may be
released, all acquired locks must be released at the end. This simple
example is described in Sec 5.2 of

http://research.microsoft.com/en-us/um/people/simonpj/papers/assoc-types/fun-with-type-funs/typefun.pdf

That example can be made more complex: a program with two locks
choosing the lock to acquire based on the data it reads from a
file. We can still statically guarantee that all acquired locks are
released and no lock is acquired or released twice -- even if we
cannot statically tell which particular lock will be acquired during a
program run.  Other examples of resource control include session types
and regions. There are several Hackage packages with these keywords.

Generally, Haskell can easily embed languages with dependent or linear
types -- just as easily as Haskell embeds languages with IO, global
mutable state, non-determinism. The latter languages go by the name of
monads. One can easily embed typed linear lambda-calculus, with
Haskell type-checker ensuring that each bound variable is referenced
exactly once.

http://okmij.org/ftp/tagless-final/course/index.html#linear

The linear lambda-calculus turns out not very useful; no wonder Girard
had to add exponentials.


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Categorical description of systems with dependent types

[Petr Pudlak]

Hi,

thanks to all who gave me valuable pointers to what to study. It will 
take me some time to absorb that, but it helped a lot.


Best regards,
Petr

On Thu, Dec 02, 2010 at 02:25:41PM -0500, Dan Doel wrote:

On Thursday 02 December 2010 10:13:32 am Petr Pudlak wrote:

  Hi,

recently, I was studying how cartesian closed categories can be used to
describe typed functional languages. Types are objects and morphisms are
functions from one type to another.

Since I'm also interested in systems with dependent types, I wonder if
there is a categorical description of such systems. The problem (as I
see it) is that the codomain of a function depends on a value passed to
the function.

I'd happy if someone could give me some pointers to some papers or other
literature.


There are many different approaches to modelling dependent types in category
theory. Roughly, they are all similar to modelling logic, but they all differ
in details.

I think the easiest one to get a handle on is locally Cartesian closed
categories, although there's some non-intuitive stuff if you're used to type
theory. The way it works is this: a locally Cartesian closed category C is a
category such that all its slice categories are cartesian closed. This gets
you the following stuff:

---

Since C is isomorphic to C/1, where 1 is a terminal object, C is itself
Cartesian closed assuming said 1 exists. This may be taken as a defining
quality as well, I forget.

---

Each slice category C/A should be viewed as the category of A-indexed families
of types. This seems kind of backwards at first, since the objects of C/A are
pairs like (X, f : X - A). However, the way of interpreting such f as a
family of types F : A - * is that F a corresponds to the 'inverse image' of f
over a. So X is supposed to be like the disjoint union of the family F in
question, and f identifies the index of any particular 'element' of X.

Why is this done? It has nicer theoretical properties. For instance, A - *
can't sensibly be a morphism, because * corresponds to the entire category of
types we're modelling. It'd have to be an object of itself, but that's
(likely) paradox-inducing.

---

Given a function f : B - A, there's a functor f* : C/A - C/B, which re-
indexes the families. If you think of this in the more usual type theory
style, it's just composition: B -f- A -F- *. In the category theoretic case,
it's somewhat more complex, but I'll just leave it at that for now.

Now, this re-indexing functor is important. In type theories, it's usually
expected to have two adjoints:

 Σf ⊣ f* ⊣ Πf

These adjoints are the dependent sum and product. To get a base type that
looks like:

 Π x:A. B

from type theory. Here's how we go:

 B should be A-indexed, so it's an object of C/A

 For any A, there's an arrow to the terminal object ! : A - 1

 This induces the functor !* : C/1 - C/A

 This has an adjoint Π! : C/A - C/1

 C/1 is isomorphic to C, so C has an object that corresponds to Π!B, which is
 the product of the family B. This object is the type Π x:A. B

In general, ΠfX, with f : A - B, and X an A-indexed family, F : A - *, is
the B-indexed family, G : B - * for ease, where G b = Π x : f⁻¹ b. F x. That
is, the product of the sub-family of X corresponding to each b. In the case of
B = 1, this is the product of the entire family X.

This adjointness stuff is (no surprise) very similar to the way quantifiers
are handled in categorical logic.

---

That's the 10,000 foot view. I wouldn't worry if you don't understand much of
the above. It isn't easy material. In addition to locally Cartesian closed
categories, you have:

 toposes
 hyperdoctrines
 categories with families
 contextual categories
 fibred categories

And I'm probably forgetting several. If you read about all of these, you'll
probably notice that there are a lot of similarities, but they mostly fail to
be perfectly reducible to one another (although toposes are locally Cartesian
closed).

I don't have any recommendations on a best introduction for learning this.
Some that I've read are:

 From Categories with Families to Locally Cartesian Closed Categories
 Locally Cartesian Closed Categories and Type Theory

but I can't say that any one paper made everything snap into place. More that
reading quite a few gradually soaked in. And I still feel rather hazy on the
subject.

Hope that helps some.

-- Dan


signature.asc
Description: Digital signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Categorical description of systems with dependent types

[wren ng thornton]

On 12/2/10 4:47 PM, Iavor Diatchki wrote:

Hi,
You have it exactly right, and I don't think that there's a
particularly deep reason to prefer the one over the other.  It seems
that computer science people
tend to go with the (product-function) terminology, while math people
seem to prefer the (sum-product) version, but it is all largely a
matter of taste.


The product=function,sum=pair terminology comes from a certain 
interpretation of dependent types in set theory. I believe this 
originated with Per Martin-Löf's work, though I don't have any citations 
on hand.


That terminology conflicts with the standard product=pair,sum=either 
terminology of functional languages, however. So folks from a functional 
background tend to prefer: dependent function, dependent product, sum; 
whereas folks from a set-theoretic background tend to prefer product, 
sum, no name/union.


--
Live well,
~wren

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Categorical description of systems with dependent types

[Petr Pudlak]

 Hi,

recently, I was studying how cartesian closed categories can be used to 
describe typed functional languages. Types are objects and morphisms are 
functions from one type to another.


Since I'm also interested in systems with dependent types, I wonder if 
there is a categorical description of such systems. The problem (as I 
see it) is that the codomain of a function depends on a value passed to 
the function.


I'd happy if someone could give me some pointers to some papers or other 
literature.


Thanks,
Petr


signature.asc
Description: Digital signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Categorical description of systems with dependent types

[Larry Evans]

On 12/02/10 09:13, Petr Pudlak wrote:
  Hi,
 
 recently, I was studying how cartesian closed categories can be used to
 describe typed functional languages. Types are objects and morphisms are
 functions from one type to another.
 
 Since I'm also interested in systems with dependent types, I wonder if
 there is a categorical description of such systems. The problem (as I
 see it) is that the codomain of a function depends on a value passed to
 the function.
 
 I'd happy if someone could give me some pointers to some papers or other
 literature.
 
 Thanks,
 Petr

Hi Petr,

Although it's not a categorical description of dependent types (AFAICT,
but I've almost no experience in category theory), dependent types
are described by Nuprl:


http://www.cs.cornell.edu/Info/People/sfa/Nuprl/NuprlPrimitives/Xfunctionality2_doc.html

For example, on that page, there's this:

  Actually, A-B is a special form of the more general x:A-C(x). When
  A is a type and C(x) is a type-valued function (in x) over domain A,
  then a member of x:A-C(x) is a function which for an argument, a:A
  takes a value in the type C(a).

HTH.

-Larry


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Categorical description of systems with dependent types

[roconnor]

On Thu, 2 Dec 2010, Petr Pudlak wrote:


Hi,

recently, I was studying how cartesian closed categories can be used to 
describe typed functional languages. Types are objects and morphisms are 
functions from one type to another.


Since I'm also interested in systems with dependent types, I wonder if there 
is a categorical description of such systems. The problem (as I see it) is 
that the codomain of a function depends on a value passed to the function.


I'd happy if someone could give me some pointers to some papers or other 
literature.


Voevodsky talks about the category of contexts in 
http://www.mefeedia.com/watch/31778282, which I understand is described 
in more detail in Semantics of type theory : correctness, completeness, 
and independence results by Thomas Streicher.


--
Russell O'Connor  http://r6.ca/
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Categorical description of systems with dependent types

[Iavor Diatchki]

Hi,
Bart Jacobs's book Categorical Logic and Type Theory has a
categorical description of a system with dependent types (among
others).  The book is fairly advanced but it has lots of details about
the constructions.
Hope this helps,
-Iavor

On Thu, Dec 2, 2010 at 8:18 AM,  rocon...@theorem.ca wrote:
 On Thu, 2 Dec 2010, Petr Pudlak wrote:

 Hi,

 recently, I was studying how cartesian closed categories can be used to
 describe typed functional languages. Types are objects and morphisms are
 functions from one type to another.

 Since I'm also interested in systems with dependent types, I wonder if
 there is a categorical description of such systems. The problem (as I see
 it) is that the codomain of a function depends on a value passed to the
 function.

 I'd happy if someone could give me some pointers to some papers or other
 literature.

 Voevodsky talks about the category of contexts in
 http://www.mefeedia.com/watch/31778282, which I understand is described in
 more detail in Semantics of type theory : correctness, completeness, and
 independence results by Thomas Streicher.

 --
 Russell O'Connor                                      http://r6.ca/
 ``All talk about `theft,''' the general counsel of the American Graphophone
 Company wrote, ``is the merest claptrap, for there exists no property in
 ideas musical, literary or artistic, except as defined by statute.''

 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Categorical description of systems with dependent types

[Larry Evans]

On 12/02/10 11:19, Iavor Diatchki wrote:
 Hi,
 Bart Jacobs's book Categorical Logic and Type Theory has a
 categorical description of a system with dependent types (among
 others).  The book is fairly advanced but it has lots of details about
 the constructions.
 Hope this helps,
 -Iavor
 

Page 586 of Jacobs' book mentions dependent products and dependent sums.
What confuses me is that Nuprl defines the dependent product as
a dependent function:


http://www.cs.cornell.edu/Info/People/sfa/Nuprl/NuprlPrimitives/Xfunctionality2_doc.html

and the dependent sum as the dependent product:


http://www.cs.cornell.edu/Info/People/sfa/Nuprl/NuprlPrimitives/Xpairs_doc.html

I sorta see that because the disjoint sum (i.e. the dependent product
in Nuprl terms) is actually a pair of values, the discriminant (1st
part) and the value whose type depends on the value of the discriminant.
And I can see Nuprl's choice to call the dependent product as a
dependent function because passing an index to this function returns
a value whose type is dependent on the index. This is just like
the value constructed by a haskell datatypes with field labels:

  data Record = MkRec { f1::T1, f2::T2, ..., fn::Tn }
  r = MkRec{ f1 = t1, f2 = t2,..., fn = tn}

However, instead of r as the dependent function, the fields are the
functions:

   fi r :: Ti,  for i=1...n

instead of Nuprl's notion:

   r fi :: Ti,  for i=1...n

Anybody know a good reason why the categorical and nuprl terms
differ, leading, to (at least in my case) a bit of confusion?


-Larry




___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Categorical description of systems with dependent types

[Dan Doel]

On Thursday 02 December 2010 10:13:32 am Petr Pudlak wrote:
   Hi,
 
 recently, I was studying how cartesian closed categories can be used to
 describe typed functional languages. Types are objects and morphisms are
 functions from one type to another.
 
 Since I'm also interested in systems with dependent types, I wonder if
 there is a categorical description of such systems. The problem (as I
 see it) is that the codomain of a function depends on a value passed to
 the function.
 
 I'd happy if someone could give me some pointers to some papers or other
 literature.

There are many different approaches to modelling dependent types in category 
theory. Roughly, they are all similar to modelling logic, but they all differ 
in details.

I think the easiest one to get a handle on is locally Cartesian closed 
categories, although there's some non-intuitive stuff if you're used to type 
theory. The way it works is this: a locally Cartesian closed category C is a 
category such that all its slice categories are cartesian closed. This gets 
you the following stuff:

---

Since C is isomorphic to C/1, where 1 is a terminal object, C is itself 
Cartesian closed assuming said 1 exists. This may be taken as a defining 
quality as well, I forget.

---

Each slice category C/A should be viewed as the category of A-indexed families 
of types. This seems kind of backwards at first, since the objects of C/A are 
pairs like (X, f : X - A). However, the way of interpreting such f as a 
family of types F : A - * is that F a corresponds to the 'inverse image' of f 
over a. So X is supposed to be like the disjoint union of the family F in 
question, and f identifies the index of any particular 'element' of X.

Why is this done? It has nicer theoretical properties. For instance, A - * 
can't sensibly be a morphism, because * corresponds to the entire category of 
types we're modelling. It'd have to be an object of itself, but that's 
(likely) paradox-inducing.

---

Given a function f : B - A, there's a functor f* : C/A - C/B, which re-
indexes the families. If you think of this in the more usual type theory 
style, it's just composition: B -f- A -F- *. In the category theoretic case, 
it's somewhat more complex, but I'll just leave it at that for now.

Now, this re-indexing functor is important. In type theories, it's usually 
expected to have two adjoints:

  Σf ⊣ f* ⊣ Πf

These adjoints are the dependent sum and product. To get a base type that 
looks like:

  Π x:A. B

from type theory. Here's how we go:

  B should be A-indexed, so it's an object of C/A

  For any A, there's an arrow to the terminal object ! : A - 1

  This induces the functor !* : C/1 - C/A

  This has an adjoint Π! : C/A - C/1

  C/1 is isomorphic to C, so C has an object that corresponds to Π!B, which is
  the product of the family B. This object is the type Π x:A. B

In general, ΠfX, with f : A - B, and X an A-indexed family, F : A - *, is 
the B-indexed family, G : B - * for ease, where G b = Π x : f⁻¹ b. F x. That 
is, the product of the sub-family of X corresponding to each b. In the case of 
B = 1, this is the product of the entire family X.

This adjointness stuff is (no surprise) very similar to the way quantifiers 
are handled in categorical logic.

---

That's the 10,000 foot view. I wouldn't worry if you don't understand much of 
the above. It isn't easy material. In addition to locally Cartesian closed 
categories, you have:

  toposes
  hyperdoctrines
  categories with families
  contextual categories
  fibred categories

And I'm probably forgetting several. If you read about all of these, you'll 
probably notice that there are a lot of similarities, but they mostly fail to 
be perfectly reducible to one another (although toposes are locally Cartesian 
closed).

I don't have any recommendations on a best introduction for learning this. 
Some that I've read are:

  From Categories with Families to Locally Cartesian Closed Categories
  Locally Cartesian Closed Categories and Type Theory

but I can't say that any one paper made everything snap into place. More that 
reading quite a few gradually soaked in. And I still feel rather hazy on the 
subject.

Hope that helps some.

-- Dan

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Categorical description of systems with dependent types

[Iavor Diatchki]

Hi,
You have it exactly right, and I don't think that there's a
particularly deep reason to prefer the one over the other.  It seems
that computer science people
tend to go with the (product-function) terminology, while math people
seem to prefer the (sum-product) version, but it is all largely a
matter of taste.
-Iavor


On Thu, Dec 2, 2010 at 11:03 AM, Larry Evans cppljev...@suddenlink.net wrote:
 On 12/02/10 11:19, Iavor Diatchki wrote:
 Hi,
 Bart Jacobs's book Categorical Logic and Type Theory has a
 categorical description of a system with dependent types (among
 others).  The book is fairly advanced but it has lots of details about
 the constructions.
 Hope this helps,
 -Iavor


 Page 586 of Jacobs' book mentions dependent products and dependent sums.
 What confuses me is that Nuprl defines the dependent product as
 a dependent function:


 http://www.cs.cornell.edu/Info/People/sfa/Nuprl/NuprlPrimitives/Xfunctionality2_doc.html

 and the dependent sum as the dependent product:


 http://www.cs.cornell.edu/Info/People/sfa/Nuprl/NuprlPrimitives/Xpairs_doc.html

 I sorta see that because the disjoint sum (i.e. the dependent product
 in Nuprl terms) is actually a pair of values, the discriminant (1st
 part) and the value whose type depends on the value of the discriminant.
 And I can see Nuprl's choice to call the dependent product as a
 dependent function because passing an index to this function returns
 a value whose type is dependent on the index. This is just like
 the value constructed by a haskell datatypes with field labels:

  data Record = MkRec { f1::T1, f2::T2, ..., fn::Tn }
  r = MkRec{ f1 = t1, f2 = t2,..., fn = tn}

 However, instead of r as the dependent function, the fields are the
 functions:

   fi r :: Ti,  for i=1...n

 instead of Nuprl's notion:

   r fi :: Ti,  for i=1...n

 Anybody know a good reason why the categorical and nuprl terms
 differ, leading, to (at least in my case) a bit of confusion?


 -Larry




 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Categorical description of systems with dependent types

[Larry Evans]

On 12/02/10 15:47, Iavor Diatchki wrote:
 Hi,
 You have it exactly right, and I don't think that there's a
 particularly deep reason to prefer the one over the other.  It seems
 that computer science people
 tend to go with the (product-function) terminology, while math people
 seem to prefer the (sum-product) version, but it is all largely a
 matter of taste.
 -Iavor
[snip]
*Maybe* the computer science people are trying to minimize the concepts.
In this case, the one concept common to both the sum and product ( in
the math peoples viewpoint) is there's a function:

   field2type: field_name - Type

in the case of a product or record, r, it's:

  product = f:fieldname - field2type(f)

in the case of a disjoint sum its:

  sum = (f:fieldname, field2type(f))

or something like that.

-Larry


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Categorical description of systems with dependent types

[Dan Doel]

On Thursday 02 December 2010 7:54:18 pm Larry Evans wrote:
 [snip]
 *Maybe* the computer science people are trying to minimize the concepts.
 In this case, the one concept common to both the sum and product ( in
 the math peoples viewpoint) is there's a function:
 
field2type: field_name - Type
 
 in the case of a product or record, r, it's:
 
   product = f:fieldname - field2type(f)
 
 in the case of a disjoint sum its:
 
   sum = (f:fieldname, field2type(f))
 
 or something like that.

I'll be honest: I don't really know what you're saying above. However, I can 
throw in my 2 cents on the naming thing.

The product-function naming obviously comes from thinking about, what if the 
type of later arguments of a tuple could depend on earlier ones, and what if 
the result type of a function could depend on the argument? These are quite 
ordinary questions for a practicing programmer to think about, which is 
probably why computer science people (supposedly) favor this naming. I might 
even use this naming myself when appropriate, although I'd say 'tuple' (or 
record) instead of 'product' to (hopefully) avoid confusion.

The sum-product naming, by contrast, comes from thinking about, we have n-ary 
sums and products for any natural n; for instance, A + B and A * B are binary. 
This can be viewed as sums and products of families of types indexed by finite 
sets. What if we generalize this to sums and products of families indexed by 
*arbitrary* types? Unlike the above, I don't think this is something that is 
likely to be sparked naturally during programming. However, it's quite close 
to similar constructions in set theory, which probably explains why 
mathematicians favor it.

If you get into category theoretic views of programming languages, I think the 
sum-product naming makes sense there, and it's hard to make the product-
function naming work. For instance:

  The A-indexed product Π x:A. F[x] has an A-indexed family of projections:
   proj a : (Π x:A. F[x]) - F[a]

  The A-indexed sum Σ x:A. F[x] has an A-indexed family of injections:
   in a : F[a] - (Σ x:A. F[x])

Which are visibly generalizations of the definitions of (co)products you'd 
encounter modelling non-dependently typed languages. Perhaps this is on the 
math end of things, though.

-- Dan

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Dependent types

[Mitar]

Hi!

I believe dependent types is the right term for my problem. I was
trying to solve it with GADTs but I was not successful so I am turning
to infinite (lazy) wisdom of Haskell Cafe.

I am attaching example code where I had to define MaybePacket data
type which combines different types of Packets I would like to allow
over Line. The problem is that there is a correlation between Line
type and MaybePacket type and I would like to tell Haskell about that.
But I am not sure how. Because now compiler, for example, warns me of
a non-exhaustive pattern even if some MaybePacket value is not
possible for given Line.

Somehow I would like to have a getFromFirstLine function which would
based on type of given Line return Maybe (Packet i) (for Line) or
Maybe AnyPacket (for LineAny). So that this would be enforced and type
checked.

Best regards and thanks for any help


Mitar


Test2.hs
Description: Binary data
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Dependent types

[Stephen Tetley]

On 10 September 2010 07:14, Mitar mmi...@gmail.com wrote:

 But I am not sure how. Because now compiler, for example, warns me of
 a non-exhaustive pattern even if some MaybePacket value is not
 possible for given Line.

This issue pops up quite quite often - Ryan Ingram's answer to it the
last time it was on the Cafe points to the relevant Trac issue
numbers:

http://www.haskell.org/pipermail/haskell-cafe/2010-August/082790.html
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Dependent types

[Mitar]

Hi!

On Fri, Sep 10, 2010 at 9:22 AM, Stephen Tetley
stephen.tet...@gmail.com wrote:
 This issue pops up quite quite often - Ryan Ingram's answer to it the
 last time it was on the Cafe points to the relevant Trac issue
 numbers:

But I have not yet made it as GADTs. I would need some help here. How
to change MaybePacket to GADTs?


Mitar
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Dependent types

[Mitar]

Hi!

I made it. ;-)

Thanks to all help from copumpkin on IRC channel.

I am attaching my solution for similar problems in future. And of
course comments.


Mitar


Test5.hs
Description: Binary data
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] dependent types

[Ben Millwood]

On Sun, Apr 11, 2010 at 10:54 PM, Jason Dagit da...@codersbase.com wrote:
 Or, you could use witness types:
 data Vehicle classification = Vehicle { ... }
 mkCar :: Vehicle Car
 mkTruck :: Vehicle Truck
 Then you would export the smart constructors, (mkCar/mkTruck) without
 exporting the Vehicle constructor.
 moveVehicle :: Vehicle c - Simulation ()
 carsOnly :: Vehicle Car - ...
 In the witness type version you may find that defining Vehicle as a GADT is
 even better:
 data Vehicle classification where
   mkCar :: ... - Vehicle Car
   mkTruck :: ... - Vehicle Truck

A minor point of syntax: GADT constructors should begin with a capital letter.
A more important point: GADT constructors are useful for some things
but aren't appropriate for this case because they aren't smart -
they can't take an Int parameter and then make either a Car or a Truck
depending on its value. A smart constructor will need to account for
the possibility that the parameter isn't valid:

mkCar :: Integer - Maybe Vehicle
mkCar weight
 | weight  carWeight = Nothing
 | otherwise = Car { weight = weight }
-- or
mkVehicle :: Integer - Vehicle
mkVehicle weight
 | weight  carWeight = Truck weight
 | otherwise = Car weight

Even with GADTs, you can't pattern match on the constructors unless
you export them, in which case you have to allow for the possibility
that someone might construct an invalid value of the type, so you
might then also need smart field labels that retrieve values from
the Vehicle without allowing you to set them as well (as you would be
able to if you exported the field label itself).

Personally I think this approach is all rather OO. The way that seems
most natural to me is:

moveVehicleAcrossBridge :: Bridge - Vehicle - Maybe Move
moveVehicleAcrossBridge bridge { maxWeight = max } vehicle { weight = w }
 | w  max = Nothing
 | otherwise = {- ... moving stuff ... -}

so you just test the properties directly as and when they are
interesting to you.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] dependent types

[Jason Dagit]

On Mon, Apr 12, 2010 at 4:32 AM, Ben Millwood hask...@benmachine.co.ukwrote:


 Personally I think this approach is all rather OO. The way that seems
 most natural to me is:

 moveVehicleAcrossBridge :: Bridge - Vehicle - Maybe Move
 moveVehicleAcrossBridge bridge { maxWeight = max } vehicle { weight = w }
  | w  max = Nothing
  | otherwise = {- ... moving stuff ... -}

 so you just test the properties directly as and when they are
 interesting to you.


The problem with this is that it doesn't address the question the OP had.
The OP's question was how to enforce things at the type level, but this,
while being a valid approach, allows heavy vehicles to attempt the bridge
crossing.  I agree it's a nice way of encoding it, but if type level
enforcement is called for then I don't see how it applies.

Jason
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] dependent types

[Anthony Cowley]

On Sun, Apr 11, 2010 at 5:54 PM, Jason Dagit da...@codersbase.com wrote:
 On Sun, Apr 11, 2010 at 1:59 AM, Andrew U. Frank
 fr...@geoinfo.tuwien.ac.at wrote:

 in modeling real application we have often the case that the type of
 some object depends on a value. e.g. small_boat is a vessel with size
 less than a constant. big_boat is a vessel with a larger size. for
 example, many legal classifications are expressed in this form (e.g. car
 vs. truck)
 depending on the type, operations are applicable or not (e.g. road with
 restriction 'no trucks').

 In the witness type version you may find that defining Vehicle as a GADT is
 even better:
 data Vehicle classification where
   mkCar :: ... - Vehicle Car
   mkTruck :: ... - Vehicle Truck
 This is nice because it's direct and when you pattern match on the
 constructor you recover the type of classification.  For example, I believe
 this would type check:
 foo :: Vehicle c - c
 foo (mkCar ...) = Car
 foo (mkTruck ...) = Truck

You can combine GADTs with a mirror type for views of that data.

{-# LANGUAGE GADTs, EmptyDataDecls #-}
module GADTSmart (VehicleView(..), Vehicle, Car, Truck,
  mkCar, mkTruck, view) where
data Car
data Truck

data Vehicle t where
VCar   :: Int - Vehicle Car
VTruck :: Int - Vehicle Truck

data VehicleView t where
VVCar   :: Int - VehicleView Car
VVTruck :: Int - VehicleView Truck

view :: Vehicle t - VehicleView t
view (VCar wt)   = VVCar wt
view (VTruck wt) = VVTruck wt

mkCar :: Int - Maybe (Vehicle Car)
mkCar wt | wt  2000 = Just (VCar wt)
 | otherwise = Nothing

mkTruck :: Int - Maybe (Vehicle Truck)
mkTruck wt | wt = 2000 = Just (VTruck wt)
   | otherwise  = Nothing


-- Client code that doesn't have access to the VCar or VTruck
-- constructors.

moveAcrossBridge :: Vehicle Car - IO ()
moveAcrossBridge c = case view c of
   VVCar wt - putStrLn $ Car (++show wt++) on bridge


Now you can type your functions with the Vehicle GADT, but only
introduce values of that type using smart constructors. You could use
the VVCar or VVTruck data constructors to create invalid values, but
they won't work your functions.

Anthony
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: dependent types

[Maciej Piechotka]

On Mon, 2010-04-12 at 12:44 -0400, Anthony Cowley wrote:
 On Sun, Apr 11, 2010 at 5:54 PM, Jason Dagit da...@codersbase.com wrote:
  On Sun, Apr 11, 2010 at 1:59 AM, Andrew U. Frank
  fr...@geoinfo.tuwien.ac.at wrote:
 
  in modeling real application we have often the case that the type of
  some object depends on a value. e.g. small_boat is a vessel with size
  less than a constant. big_boat is a vessel with a larger size. for
  example, many legal classifications are expressed in this form (e.g. car
  vs. truck)
  depending on the type, operations are applicable or not (e.g. road with
  restriction 'no trucks').
 
  In the witness type version you may find that defining Vehicle as a GADT is
  even better:
  data Vehicle classification where
mkCar :: ... - Vehicle Car
mkTruck :: ... - Vehicle Truck
  This is nice because it's direct and when you pattern match on the
  constructor you recover the type of classification.  For example, I believe
  this would type check:
  foo :: Vehicle c - c
  foo (mkCar ...) = Car
  foo (mkTruck ...) = Truck
 
 You can combine GADTs with a mirror type for views of that data.
 
 {-# LANGUAGE GADTs, EmptyDataDecls #-}
 module GADTSmart (VehicleView(..), Vehicle, Car, Truck,
   mkCar, mkTruck, view) where
 data Car
 data Truck
 
 data Vehicle t where
 VCar   :: Int - Vehicle Car
 VTruck :: Int - Vehicle Truck
 
 data VehicleView t where
 VVCar   :: Int - VehicleView Car
 VVTruck :: Int - VehicleView Truck
 
 view :: Vehicle t - VehicleView t
 view (VCar wt)   = VVCar wt
 view (VTruck wt) = VVTruck wt
 
 mkCar :: Int - Maybe (Vehicle Car)
 mkCar wt | wt  2000 = Just (VCar wt)
  | otherwise = Nothing
 
 mkTruck :: Int - Maybe (Vehicle Truck)
 mkTruck wt | wt = 2000 = Just (VTruck wt)
| otherwise  = Nothing
 
 
 -- Client code that doesn't have access to the VCar or VTruck
 -- constructors.
 
 moveAcrossBridge :: Vehicle Car - IO ()
 moveAcrossBridge c = case view c of
VVCar wt - putStrLn $ Car (++show wt++) on bridge
 
 
 Now you can type your functions with the Vehicle GADT, but only
 introduce values of that type using smart constructors. You could use
 the VVCar or VVTruck data constructors to create invalid values, but
 they won't work your functions.
 
 Anthony

http://www.willamette.edu/~fruehr/haskell/evolution.html

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
data Zero = Zero
data Succ a = Succ a

class Peano a where
fromPeano :: a - Integer

instance Peano Zero where
fromPeano _ = 0

instance forall a. Peano a = Peano (Succ a) where
fromPeano _ = 1 + fromPeano (undefined :: a)

class (Peano a, Peano b) = LT a b

instance Peano b = LT Zero (Succ b)
instance LT a b = LT a (Succ b)
instance LT a b = LT (Succ a) (Succ b)

class (Peano a, Peano b) = EQ a b
instance EQ Zero Zero
instance EQ a b = EQ (Succ a) (Succ b)

class (Peano a, Peano b) = GT a b
instance LT a b = GT b a

class (Peano a, Peano b) = LEQ a b
instance EQ a b = LEQ a b
instance LEQ a b = LEQ a (Succ b)

class (Peano a, Peano b) = GEQ a b
instance EQ a b = GEQ a b
instance GEQ a b = GEQ (Succ a) b

type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type Four = Succ Three
type Five = Succ Four

data Car = Car
data Truck = Truck

data Vehicle s v where
VCar :: LT size Five = Vehicle size Car
VTruck :: GEQ size Five = Vehicle size Truck

Regards


signature.asc
Description: This is a digitally signed message part
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] dependent types

[Andrew U. Frank]

in modeling real application we have often the case that the type of
some object depends on a value. e.g. small_boat is a vessel with size
less than a constant. big_boat is a vessel with a larger size. for
example, many legal classifications are expressed in this form (e.g. car
vs. truck)
depending on the type, operations are applicable or not (e.g. road with
restriction 'no trucks'). 
how could one model such situations in haskell? i assume there are
several possibilities...



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: dependent types

[Maciej Piechotka]

On Sun, 2010-04-11 at 10:59 +0200, Andrew U. Frank wrote:
 in modeling real application we have often the case that the type of
 some object depends on a value. e.g. small_boat is a vessel with size
 less than a constant. big_boat is a vessel with a larger size. for
 example, many legal classifications are expressed in this form (e.g. car
 vs. truck)
 depending on the type, operations are applicable or not (e.g. road with
 restriction 'no trucks'). 
 how could one model such situations in haskell? i assume there are
 several possibilities...

I'd model upper type as actuall type and dependants as newtypes of it
with hidden constructors. 

module Car
  (
Car,
vehicleToCar,
carToVehicle,
  )
where
import Vehicle

newtype Car = Car {carToVehicle :: Vehicle}

vehicleToCar :: Vehicle - Maybe Car
vehicleToCar v | someCondition = Just $! Car v
   | otherwise = Nothing



Then you can request that:

moveSomeRoad :: Either Car Bicycle - IO ()
moveSomeRoad = ...

Regards

PS.
If it is possible to define a :-: b which would change (recusivly) a
replacing Either x b into x then you can define 'Vehicle' universe.
However I know too less about type functions to say it for sure.



signature.asc
Description: This is a digitally signed message part
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] dependent types

[Jason Dagit]

On Sun, Apr 11, 2010 at 1:59 AM, Andrew U. Frank fr...@geoinfo.tuwien.ac.at
 wrote:

 in modeling real application we have often the case that the type of
 some object depends on a value. e.g. small_boat is a vessel with size
 less than a constant. big_boat is a vessel with a larger size. for
 example, many legal classifications are expressed in this form (e.g. car
 vs. truck)
 depending on the type, operations are applicable or not (e.g. road with
 restriction 'no trucks').
 how could one model such situations in haskell? i assume there are
 several possibilities...


The two main ways I can think of for this use typeclasses or witness types.

The type class way is like this:
class Vehicle a where

data Car
data Truck

instance Vehicle Car where
instance Vehicle Truck where

Now you can have things that take a Car or a Truck or they can take a
Vehicle instead.

moveVehicle :: Vehicle v = v - Simulation ()

carsOnly :: Car - ...

If you want to understand this approach better, I think this is how HList
works to some extent.  For example, see their HBool type class.

Or, you could use witness types:

data Vehicle classification = Vehicle { ... }

mkCar :: Vehicle Car
mkTruck :: Vehicle Truck

Then you would export the smart constructors, (mkCar/mkTruck) without
exporting the Vehicle constructor.

moveVehicle :: Vehicle c - Simulation ()
carsOnly :: Vehicle Car - ...

In the witness type version you may find that defining Vehicle as a GADT is
even better:

data Vehicle classification where
  mkCar :: ... - Vehicle Car
  mkTruck :: ... - Vehicle Truck

This is nice because it's direct and when you pattern match on the
constructor you recover the type of classification.  For example, I believe
this would type check:

foo :: Vehicle c - c
foo (mkCar ...) = Car
foo (mkTruck ...) = Truck

(Note: I didn't test any of the above, so I could have errors/typos.)

Jason
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] dependent types

[Ozgur Akgun]

On 11 April 2010 22:54, Jason Dagit da...@codersbase.com wrote:



...



class Vehicle a where

 data Car
 data Truck

 instance Vehicle Car where
 instance Vehicle Truck where

 Now you can have things that take a Car or a Truck or they can take a
 Vehicle instead.

 moveVehicle :: Vehicle v = v - Simulation ()


unfortunately, now you cannot use pattern matching while defining
moveVehicle.

...



Jason




-- 
Ozgur Akgun
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] dependent types

[Jason Dagit]

On Sun, Apr 11, 2010 at 4:15 PM, Ozgur Akgun ozgurak...@gmail.com wrote:


 On 11 April 2010 22:54, Jason Dagit da...@codersbase.com wrote:



 ...



 class Vehicle a where

 data Car
 data Truck

 instance Vehicle Car where
 instance Vehicle Truck where

 Now you can have things that take a Car or a Truck or they can take a
 Vehicle instead.

 moveVehicle :: Vehicle v = v - Simulation ()


 unfortunately, now you cannot use pattern matching while defining
 moveVehicle.


That's true.  Although, if you're writing a simulation where Cars and Trucks
are objects in that simulation, they are likely to be defined as records as
they will probably have many fields.  If that's the case, it's unlikely
you'd be using pattern matching with them anyway.  It's just a small step
from there to using typeclass functions to access the parts you care about.

Jason
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: Approaches to dependent types (DT)

[Benjamin Franksen]

pbrowne wrote:
 Dependent Types (DT)
 The purpose of dependent types (DT) is to allow programmers to specify
 dependencies between the parameters of a multiple parameter class.  

'Dependent type' means result type (of a function) can depend on argument 
values. This is not (directly) supported in Haskell.

What you are talking about is called 'functional dependencies', not 
'dependent types'. Sometimes abbreviated as 'fundeps'.

 DTs
 can be seen as a move towards more general purpose parametric type
 classes. 

This is at least misleading, as adding a functional dependency does not make 
the class more general, but more special, as it reduces the number of 
possible instances.

Cheers
Ben

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: Approaches to dependent types (DT)

[pbrowne]

Ben,
I have added your input. Thanks for putting me right.
Pat


Functional Dependencies
The purpose of functional dependencies (FD) is to allow programmers to
specify dependencies between the parameters of a multiple parameter
class. FD reduces the number of possible instances, or models of a
class. Note, the notion of FD is distinct from the concept of 'Dependent
types', where the result type (of a function) can depend on argument values.

FD are declared in a class header, where the type of one class
parameter is declared to depend on another class parameter. Consider the
following example:

class Named object name | object - name where
namef :: object - name

instance (Eq name, Named object name) = Eq object where
object1 == object2 = (namef object1) == (namef object2)

The first part of the class definition Named takes two type variables as
parameters; namely object and name. We say, that object determines name
or alternatively that name is determined by object. This is denoted in
the second part of the class header (i.e. | object - name). With DTs,
the dependent type depends on values of the determining type.  Hence, a
FD involves a relation between Haskell’s value-level and the type-level
(or type system). The Named class contains the signature, but not the
definition, of one function called namef. Note, the in the definition of
namef, the argument and return type (object - name) are textually
identical to that occurring in the class header, however the semantic is
that of function definition rather that of type dependency.
In the instance declaration, the part before the = is called the
context, while the part after the = is called the head of the instance
declaration. The context contains one or more class assertions, which is
a list of classes each with their respective type variables, asserting
that a type variable is a parameter of a particular class. The context
for the above example includes two previously defined classes. The Eq
class is defined in the Haskell prelude and our user defined Named
class.  The instance asserts:
If  (type of name is an instance of the Eq class) and
 (type pair (object, name) is an instance of  Named)  then
  object is an instance of Eq
The new Eq instance defined is quite general, it asserts that every type
object is
an instance of the Eq class.  It does not say that every type object
that is an instance of Named is also an instance of Eq.
Now we consider the definition of equality (==) for the type object in
the instance body. Initially, the definition determines the type name in
a type-type dependency (e.g. via the function call namef object1). When
the two names have been calculated the function uses this information to
define equality on values of type  object via equality on values of type
name.



Benjamin Franksen wrote:
 pbrowne wrote:
 Dependent Types (DT)
 The purpose of dependent types (DT) is to allow programmers to specify
 dependencies between the parameters of a multiple parameter class.  
 
 'Dependent type' means result type (of a function) can depend on argument 
 values. This is not (directly) supported in Haskell.
 
 What you are talking about is called 'functional dependencies', not 
 'dependent types'. Sometimes abbreviated as 'fundeps'.
 
 DTs
 can be seen as a move towards more general purpose parametric type
 classes. 
 
 This is at least misleading, as adding a functional dependency does not make 
 the class more general, but more special, as it reduces the number of 
 possible instances.
 
 Cheers
 Ben
 
 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Approaches to dependent types (DT)

[pbrowne]

Hi,
I am attempting to explain an example of dependent types to computing
practitioners who do not have any background in functional programming.
My goal is to explain the example rather than implement or improve it. I
have been told in previous postings that the approach below is a bit
dated. Any comments on the correctness or otherwise would be appreciated.

Regards,
Pat

===

Dependent Types (DT)
The purpose of dependent types (DT) is to allow programmers to specify
dependencies between the parameters of a multiple parameter class.  DTs
can be seen as a move towards more general purpose parametric type
classes. DTs are declared in a class header, where the type of one class
parameter is declared to depend on another class parameter. Consider the
following example:

class Named object name | object - name where
namef :: object - name

instance (Eq name, Named object name) = Eq object where
object1 == object2 = (namef object1) == (namef object2)

The first part of the class definition Named takes two type variables as
parameters; namely object and name. We say, that object determines name
or alternatively that name is determined by object. This is denoted in
the second part of the class header (i.e. | object - name). With DTs,
the dependent type depends on values of the determining type.  Hence, a
DT involves a relation between Haskell’s value-level and the type-level
(or type system). The Named class contains the signature, but not the
definition, of one function called namef. Note, the in the definition of
namef, the argument and return type (object - name) are textually
identical to that occurring in the class header, however the semantic is
that of function definition rather that of type dependency.
In the instance declaration, the part before the = is called the
context, while the part after the = is called the head of the instance
declaration. The context contains one or more class assertions, which is
a list of classes each with their respective type variables, asserting
that a type variable is a parameter of a particular class. The context
for the above example includes two previously defined classes. The Eq
class is defined in the Haskell prelude and our user defined Named
class.  The instance asserts:
If  (type of name is an instance of the Eq class) and
 (type pair (object, name) is an instance of  Named)  then
  object is an instance of Eq
The Eq instance is quite general, it asserts that every type object is
an instance of the Eq class.  It does not say that every type object
that is an instance of Named is also an instance of Eq.
Now we consider the definition of equality (==) for the type object in
the instance body. Initially, the definition determines the type name in
a type-type dependency (e.g. via the function call namef object1). When
the two names have been calculated the function uses this information to
define equality on values of type  object via equality on values of type
name.



















Dan Doel wrote:
 I'll see if I can't gloss over some of the stuff Ryan Ingram already covered.
 
 On Friday 09 October 2009 9:11:30 am pat browne wrote:
 2) Types depending on types called parametric and type-indexed types
 
 The above distinction in types (and values) depending on types has to do with 
 operations beyond just said dependency. For instance:
 
   data List a = Nil | Cons a (List a)
 
 Is the definition involving types that depend on other types. And similarly:
 
   foo :: forall a. List (List a)
   foo = Cons Nil Nil
 
 is a value that depends on a type. In a language more explicit about type 
 application, one might write:
 
   f...@a = Cons@(List a) n...@a Nil@(List a)
 
 So far, these fall in the parametric category, but your example does not:
 
 class Named object name | object - name where
 name :: object - name
 
 Classes in H98 allow you to define non-parametric type-value dependence, and 
 when extended with functional dependencies, or alternately, if we consider 
 type families, we get non-parametric type-type dependence. The difference 
 isn't in what things can depend on what other things, but in what operations 
 are available on types. Specifically, type classes/families are like being 
 able to do case analysis on types, so in the value case:
 
   class Foo a where
 bar :: [a]
 
   instance Foo Int where
 bar = [5]
 
   instance Foo Char where
 bar = c
 
 can be seen as similar to:
 
   b...@c = typecase c of
 Int  - [5]
 Char - c
 
 And type families are similar on the type-level (it's less clear how 
 functional dependencies fit in, but a one way a - b is kind of like doing a 
 type-level typecase on a to define b; more accurately you have multiple type 
 parameters, but in each a-branch, b there is exactly one b-branch). Of 
 course, 
 this is an over-simplification, so take it with salt.
 
 I am aware that dependent types can

Re: [Haskell-cafe] Approaches to dependent types (DT)

[pat browne]

Petr,
Thanks for the links. My research involves the study of current
algebraic specification and programming languages.
I have posted some very general and abstract style questions in order to
get a better feel of the individual languages.
I do not wish to become highly proficient in each language, so any links
that speed up my research are much appreciated.

Thanks again,
Pat




Petr Pudlak wrote:
 Hi Pat,
 
 you might be interested in Agda [1] and the tutorial Dependently Typed
 Programming in Agda [2]. I'm just reading the tutorial and it helps me
 a lot with understanding the concept.
 
 Also if you'd like to have a deeper understanding of the underlying
 theory, I'd suggest reading Barendregt's Lambda Calculi with Types
 [3].
 
 Best regards,
   Petr
 
 [1] http://wiki.portal.chalmers.se/agda/
 [2] http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf
 [3] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.4391
 and ftp://ftp.cs.kun.nl/pub/CompMath.Found/HBKJ.ps.Z
 
 On Fri, Oct 09, 2009 at 02:11:30PM +0100, pat browne wrote:
 Hi,
 I am trying to understand the concept of dependent types as described in
 Haskell literature (Hallgren 2001),(Hinze,Jeuring et al. 2006). I am
 particularly interested in understanding two flavours of dependency
 mentioned by Hinze et al:
 1) Types depending on values called dependent types
 2) Types depending on types called parametric and type-indexed types

 I think that ascending levels of abstraction are important here: values
 - types - classes (Hallgren 2001). Here is a Haskell example of the use
 of DT:

 class Named object name | object - name where
 name :: object - name

 instance (Eq name, Named object name) = Eq object where
 object1 == object2 = (name object1) == (name object2)

 I think that the intended semantics are:
 1) Objects have names  and can be compared for equality using these names.
 2) Two objects are considered equal (identical) if they have the same name.
 3) The type of a name depends on the type of the object, which gets
 expressed as a type dependency (object - name).
 I am not sure about the last semantic it might be interpreted as the
 named object depends on... This may indicate a flaw in my understanding
 of DT.

 I am aware that dependent types can be used to express constraints on
 the size of lists and other collections. My understanding of Haskell's
 functional dependency is that object - name indicates that fixing the
 type object should fix the type name (equivalently we could say that
 type name depends on type object). The class definition seems to show a
 *type-to-type* dependency (object to name), while the instance
 definition shows how a name value is used to define equality for objects
 which could be interpreted as a *value-to-type* dependency (name to
 object) in the opposite direction to that of the class.

 My questions are:
 Question 1: Is my understanding correct?
 Question 2: What flavour of DT is this does this example exhibit?

 Best regards,
 Pat


 Hallgren, T. (2001). Fun with Functional Dependencies. In the
 Proceedings of the Joint CS/CE Winter Meeting, Varberg, Sweden, January
 2001.
 Hinze, R., J. Jeuring, et al. (2006). Comparing Approaches to Generic
 Programming in Haskell. Datatype-generic programming: international
 spring school, SSDGP 2006.

 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Approaches to dependent types (DT)

[Dan Doel]

I'll see if I can't gloss over some of the stuff Ryan Ingram already covered.

On Friday 09 October 2009 9:11:30 am pat browne wrote:
 2) Types depending on types called parametric and type-indexed types

The above distinction in types (and values) depending on types has to do with 
operations beyond just said dependency. For instance:

  data List a = Nil | Cons a (List a)

Is the definition involving types that depend on other types. And similarly:

  foo :: forall a. List (List a)
  foo = Cons Nil Nil

is a value that depends on a type. In a language more explicit about type 
application, one might write:

  f...@a = Cons@(List a) n...@a Nil@(List a)

So far, these fall in the parametric category, but your example does not:

 class Named object name | object - name where
 name :: object - name

Classes in H98 allow you to define non-parametric type-value dependence, and 
when extended with functional dependencies, or alternately, if we consider 
type families, we get non-parametric type-type dependence. The difference 
isn't in what things can depend on what other things, but in what operations 
are available on types. Specifically, type classes/families are like being 
able to do case analysis on types, so in the value case:

  class Foo a where
bar :: [a]

  instance Foo Int where
bar = [5]

  instance Foo Char where
bar = c

can be seen as similar to:

  b...@c = typecase c of
Int  - [5]
Char - c

And type families are similar on the type-level (it's less clear how 
functional dependencies fit in, but a one way a - b is kind of like doing a 
type-level typecase on a to define b; more accurately you have multiple type 
parameters, but in each a-branch, b there is exactly one b-branch). Of course, 
this is an over-simplification, so take it with salt.

 I am aware that dependent types can be used to express constraints on
 the size of lists and other collections.

Technically, you don't need dependent types for this, you just need type-level 
naturals. But dependent types (or some sufficiently fancy faking thereof) are 
nice in that you only need to define the naturals once, instead of at both the 
value and type levels.

 The class definition seems to show a
 *type-to-type* dependency (object to name), while the instance
 definition shows how a name value is used to define equality for objects
 which could be interpreted as a *value-to-type* dependency (name to
 object) in the opposite direction to that of the class.

As Ryan remarked, this is not a value-type dependency. In the instance, you 
are defining equality for the type 'object' which determines the type 'name' 
in a type-type dependency. You're then defining equality on values of type 
'object' via equality on values of type 'name', via the 'name' function. But 
that's just value-value dependency which every language of course has.

GHC does have ways of faking dependent types, though, with GADTs. GADTs allow 
you to define data such that matching on constructors refines things in the 
type system. So, along with the mirroring mentioned above, you can manually 
set up a value-type dependency that acts like full-on dependent types. For 
naturals it looks like:

  -- type level naturals
  data Zero
  data Suc n

  -- value-level GADT indexed by the type-level naturals
  data Nat n where
Zero :: Nat Zero
Suc  :: Nat n - Nat (Suc n)

  -- existential wrapper
  data Natural where
Wrap :: Nat n - Natural

Ryan's zip function would look like:

  zip :: forall a b n. Nat n - Vector n a - Vector n b - Vector n (a,b)
  zip ZeroNil Nil = Nil
  zip (Suc n) (Cons x xs) (Cons y ys) = Cons (x,y) (zip n xs ys)

although the 'Nat n' parameter is technically unnecessary in this case. But, 
in some other function:

  foo :: forall n. Nat n - T
  foo Zero= {- we know type-level n = Zero here -}
  foo (Suc n) = {- we know type-level n = Suc m for some m here -}

Of course, mirroring like the above is kind of a pain and only gets more so 
the more complex the things you want to mirror are (although this is how, for 
instance, ATS handles dependent types). There is a preprocessor, SHE, that 
automates this, though, and lets you write definitions that look like a full-
on dependently typed language (among other things).

Anyhow, I'll cease rambling for now.

Cheers,

-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Approaches to dependent types (DT)

[pat browne]

Hi,
I am trying to understand the concept of dependent types as described in
Haskell literature (Hallgren 2001),(Hinze,Jeuring et al. 2006). I am
particularly interested in understanding two flavours of dependency
mentioned by Hinze et al:
1) Types depending on values called dependent types
2) Types depending on types called parametric and type-indexed types

I think that ascending levels of abstraction are important here: values
- types - classes (Hallgren 2001). Here is a Haskell example of the use
of DT:

class Named object name | object - name where
name :: object - name

instance (Eq name, Named object name) = Eq object where
object1 == object2 = (name object1) == (name object2)

I think that the intended semantics are:
1) Objects have names  and can be compared for equality using these names.
2) Two objects are considered equal (identical) if they have the same name.
3) The type of a name depends on the type of the object, which gets
expressed as a type dependency (object - name).
I am not sure about the last semantic it might be interpreted as the
named object depends on... This may indicate a flaw in my understanding
of DT.

I am aware that dependent types can be used to express constraints on
the size of lists and other collections. My understanding of Haskell's
functional dependency is that object - name indicates that fixing the
type object should fix the type name (equivalently we could say that
type name depends on type object). The class definition seems to show a
*type-to-type* dependency (object to name), while the instance
definition shows how a name value is used to define equality for objects
which could be interpreted as a *value-to-type* dependency (name to
object) in the opposite direction to that of the class.

My questions are:
Question 1: Is my understanding correct?
Question 2: What flavour of DT is this does this example exhibit?

Best regards,
Pat


Hallgren, T. (2001). Fun with Functional Dependencies. In the
Proceedings of the Joint CS/CE Winter Meeting, Varberg, Sweden, January
2001.
Hinze, R., J. Jeuring, et al. (2006). Comparing Approaches to Generic
Programming in Haskell. Datatype-generic programming: international
spring school, SSDGP 2006.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Approaches to dependent types (DT)

[Ryan Ingram]

On Fri, Oct 9, 2009 at 6:11 AM, pat browne patrick.bro...@comp.dit.iewrote:

 class Named object name | object - name where
 name :: object - name

 instance (Eq name, Named object name) = Eq object where
 object1 == object2 = (name object1) == (name object2)


This is a type-indexed type.  On a modern GHC I would write it this way:

class Named a where
   type Name a
   name :: a - Name a

instance (Named a, Eq (Name a)) = Eq a where
   o1 == o2 = name o1 == name o2

Although to be honest I wouldn't write it this way at all, because your Eq
instance is too general (remember, constraints are not examined when doing
typeclass resolution; you are not saying every type 'a' that is an instance
of Named with Eq (Name a) is also an instance of Eq, you are saying EVERY
type 'a' is an instance of Eq, and please add the additional constraints 'Eq
(Name a)' and 'Named a')


 My questions are:
 Question 1: Is my understanding correct?
 Question 2: What flavour of DT is this does this example exhibit?


When you say Dependent Types, what is usually meant is that types can
depend on *values*; for example:

data Vector :: Integer - * - * where
Nil :: Vector 0 a
Cons :: a - Vector n a - Vector (n+1) a

Now you might write this function:

zip :: forall a b. (n :: Integer) - Vector n a - Vector n b - Vector n
(a,b)
zip 0 Nil Nil = Nil
zip (n+1) (Cons x xs) (Cons y ys) = Cons (x,y) (zip n xs ys)

Notice that the *type* Vector n a depends on the *value* of the argument 'n'
passed in.  Normally it is only the other way around; values are limited by
what type they are.  Here we have types being affected by some object's
value!

  -- ryan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Free theorems for dependent types?

[Eugene Kirpichov]

Thanks for the thorough response.

I've found BarrasBernardo's work (at least, slides) about ICC*, I'll
have a look at it.
Could you provide with names of works by Altenkirch/Morris/Oury/you?
The unordered pair example was especially interesting, since I am
somewhat concerned with which operations do not break parametricity
for *unordered sets* (as opposed to lists) - turns out, not too many.


2009/5/18 Conor McBride co...@strictlypositive.org:
 Hi

 Questions of parametricity in dependent types are made more
 complex by the way in which the Pi-type

  (x : S) - T

 corresponds to universal quantification. It's good to think
 of this type as a very large product, tupling up individual
 T's for each possible x you can distinguish by observation.
 For all x here means For each individual x.

 By contrast, your typical universally quantified type

  forall x. t

 gives you fantastic guarantees of ignorance about x! It's
 really a kind of intersection. For all x here means
 For a minimally understood x --- your program should work
 even when x is replaced by a cardboard cutout rather than
 an actual whatever-it-is, and this guarantees the
 uniformity of operation which free theorems exploit.
 I'm reminded of the Douglas Adams line We demand rigidly
 defined areas of doubt and uncertainty..

 In the dependent case, how much uniformity you get depends
 on what observations are permitted on the domain. So what's
 needed, to get more theorems out, is a richer language of
 controlled ignorance. There are useful developments:

  (1) Barras and Bernardo have been working on a dependent
    type system which has both of the above foralls, but
    distinguishes them. As you would hope, the uniform
    forall, its lambda, and application get erased between
    typechecking and execution. We should be hopeful for
    parametricity results as a consequence.

  (2) Altenkirch, Morris, Oury, and I have found a way
    (two, in fact, and there's the rub) to deliver
    quotient structures, which should allow us to specify
    more precisely which observations are available on a
    given set. Hopefully, this will facilitate parametric
    reasoning --- if you can only test this, you're bound
    to respect that, etc. My favourite example is the
    recursion principle on *unordered* pairs of numbers
    (N*N/2).

    uRec :
    (P : N*N/2 - Set) -
    ((y : N) - P (Zero, y)) -
    ((xy : N*N/2) - P xy - P (map Suc xy)) -
    (xy : N*N/2) - P xy

    Given an unordered pair of natural numbers, either
    one is Zero or both are Suc, right? You can define
    some of our favourite operators this way.

    add  = uRec (\ _ - N) (\ y - y) (\ _ - Suc . Suc)
    max  = uRec (\ _ - N) (\ y - y) (\ _ - Suc)
    min  = uRec (\ _ - N) (\ y - y) (\ _ - id)
    (==) = uRec (\ _ - Bool) isZero (\ _ - id)

    I leave multiplication as an exercise.

    The fact that these operators are commutative is
    baked into their type.

 To sum up, the fact that dependent types are good at
 reflection makes them bad at parametricity, but there's
 plenty of work in progress aimed at the kind of information
 hiding which parametricity can then exploit.

 There are good reasons to be optimistic here.

 All the best

 Conor

 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe




-- 
Eugene Kirpichov
Web IR developer, market.yandex.ru
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Free theorems for dependent types?

[Eugene Kirpichov]

Thanks, at least the title looks like exactly what I've been looking
for, however I cannot quickly appreciate the notation-heavy contents:
I definitely will as soon as possible.

2009/5/20 Masahiro Sakai masahiro.sa...@gmail.com:
 From: Eugene Kirpichov ekirpic...@gmail.com
 Date: Sun, 17 May 2009 23:10:12 +0400

 Is there any research on applying free theorems / parametricity to
 type systems more complex than System F; namely, Fomega, or calculus
 of constructions and alike?

 You may be interested in this:
 The Theory of Parametricity in Lambda Cube by Takeuti Izumi
 http://www.m.is.sci.toho-u.ac.jp/~takeuti/abs-e.html#cube

 -- Masahiro Sakai
 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe




-- 
Eugene Kirpichov
Web IR developer, market.yandex.ru
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Free theorems for dependent types?

[Conor McBride]

Hi

On 20 May 2009, at 07:08, Eugene Kirpichov wrote:


Thanks for the thorough response.

I've found BarrasBernardo's work (at least, slides) about ICC*, I'll
have a look at it.
Could you provide with names of works by Altenkirch/Morris/Oury/you?
The unordered pair example was especially interesting, since I am
somewhat concerned with which operations do not break parametricity
for *unordered sets* (as opposed to lists) - turns out, not too many.


Unordered sets or bags? Both are interesting, but hiding
multiplicity makes sets tricky.

Anyway, the news on publications is not so good. There's a
paper

  Observational Equality, Now! by Altenkirch, McB, Swierstra

which describes more or less how we handle observational
equalities in general, but the specific instantiation of that
pattern to quotients is more recent. An older paper

  Constructing Polymorphic Programs with Quotient Types by
 Abbott, Altenkirch, McB, Ghani

extends container theory to things which are fuzzy about
position (bags, cycles, etc), so may have some relevance.

One formulation of quotients in Epigram 2, by the aforementioned
Altenkirch, Morris, McB, Oury, are sadly documented only by the
source code of the implementation, which you can find here

  http://www.e-pig.org/darcs/epigram/src/Quotient.lhs

if you're curious. We knocked that up in about half an hour
one afternoon shortly before the money ran out.

The basic idea is terribly simple. A quotient is an abstract
type X/f wrapping a carrier set X which has a notion of normal
form given by f : X - Y, for some Y. (e.g. f might be even,
and Y Bool, giving arithmetic modulo 2). Equality on X/f
is just equality at Y of whatever f gives on the packed C
values. You can almost unpack X/f freely, gaining access to
the element of the carrier, applying any (possibly dependent)
function g you like to it -- just as long as you can prove that

  forall x x'. f x == f x' - g x == g x'

Any such g on X readily lifts to X/f. This to design and
redesign an interface of quotient-respecting functions and then
work compositionally.

Amusingly, under certain circumstances, the idea of quotient by
an equivalence fits this picture: given R : X - X - Prop, just
take Y, above, to be X - Prop (a predicate describing an
equivalence class; predicates are equal by mutual inclusion).
That allows you permutative quotients which don't admit a more
concrete normal form, like general unordered pairs. Of course,
if you do have an order on the data, you can just take f to be
sort!

Sorry for lack of writings, for which this status dump is poor
compensation. Things aren't very applied yet, but the machinery
for restricting observation in exchange for guarantees is on its
way. We'll see what the summer brings.

All the best

Conor

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Free theorems for dependent types?

[Eugene Kirpichov]

Or in a language without bottoms.

2009/5/20 David Menendez d...@zednenem.com:
 On Sun, May 17, 2009 at 11:52 PM, Ryan Ingram ryani.s...@gmail.com wrote:
 Free theorem's are theorems about functions that rely only on parametricity.

 For example, consider any function f with the type
   forall a. a - a

 From its type, I can tell you directly that this theorem holds:
  forall g :: A - B, x :: A,
      f (g  x) = g (f x)

 (Note that the f on the left is B - B, the f on the right is A - A).

 Note also that the theorem only holds in a strict language (i.e., not 
 Haskell).

 data A = A deriving Show
 data B = B deriving Show

 f :: a - a
 f = const undefined

 g :: A - B
 g = const B

 *Main f (g A)
 *** Exception: Prelude.undefined
 *Main g (f A)
 B

 --
 Dave Menendez d...@zednenem.com
 http://www.eyrie.org/~zednenem/
 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe




-- 
Eugene Kirpichov
Web IR developer, market.yandex.ru
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Free theorems for dependent types?

[David Menendez]

On Sun, May 17, 2009 at 11:52 PM, Ryan Ingram ryani.s...@gmail.com wrote:
 Free theorem's are theorems about functions that rely only on parametricity.

 For example, consider any function f with the type
   forall a. a - a

 From its type, I can tell you directly that this theorem holds:
  forall g :: A - B, x :: A,
      f (g  x) = g (f x)

 (Note that the f on the left is B - B, the f on the right is A - A).

Note also that the theorem only holds in a strict language (i.e., not Haskell).

data A = A deriving Show
data B = B deriving Show

f :: a - a
f = const undefined

g :: A - B
g = const B

*Main f (g A)
*** Exception: Prelude.undefined
*Main g (f A)
B

-- 
Dave Menendez d...@zednenem.com
http://www.eyrie.org/~zednenem/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Free theorems for dependent types?

[Masahiro Sakai]

From: Eugene Kirpichov ekirpic...@gmail.com
Date: Sun, 17 May 2009 23:10:12 +0400

 Is there any research on applying free theorems / parametricity to
 type systems more complex than System F; namely, Fomega, or calculus
 of constructions and alike?

You may be interested in this:
The Theory of Parametricity in Lambda Cube by Takeuti Izumi
http://www.m.is.sci.toho-u.ac.jp/~takeuti/abs-e.html#cube

-- Masahiro Sakai
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Free theorems for dependent types?

[Conor McBride]

Hi

Questions of parametricity in dependent types are made more
complex by the way in which the Pi-type

  (x : S) - T

corresponds to universal quantification. It's good to think
of this type as a very large product, tupling up individual
T's for each possible x you can distinguish by observation.
For all x here means For each individual x.

By contrast, your typical universally quantified type

  forall x. t

gives you fantastic guarantees of ignorance about x! It's
really a kind of intersection. For all x here means
For a minimally understood x --- your program should work
even when x is replaced by a cardboard cutout rather than
an actual whatever-it-is, and this guarantees the
uniformity of operation which free theorems exploit.
I'm reminded of the Douglas Adams line We demand rigidly
defined areas of doubt and uncertainty..

In the dependent case, how much uniformity you get depends
on what observations are permitted on the domain. So what's
needed, to get more theorems out, is a richer language of
controlled ignorance. There are useful developments:

  (1) Barras and Bernardo have been working on a dependent
type system which has both of the above foralls, but
distinguishes them. As you would hope, the uniform
forall, its lambda, and application get erased between
typechecking and execution. We should be hopeful for
parametricity results as a consequence.

  (2) Altenkirch, Morris, Oury, and I have found a way
(two, in fact, and there's the rub) to deliver
quotient structures, which should allow us to specify
more precisely which observations are available on a
given set. Hopefully, this will facilitate parametric
reasoning --- if you can only test this, you're bound
to respect that, etc. My favourite example is the
recursion principle on *unordered* pairs of numbers
(N*N/2).

uRec :
(P : N*N/2 - Set) -
((y : N) - P (Zero, y)) -
((xy : N*N/2) - P xy - P (map Suc xy)) -
(xy : N*N/2) - P xy

Given an unordered pair of natural numbers, either
one is Zero or both are Suc, right? You can define
some of our favourite operators this way.

add  = uRec (\ _ - N) (\ y - y) (\ _ - Suc . Suc)
max  = uRec (\ _ - N) (\ y - y) (\ _ - Suc)
min  = uRec (\ _ - N) (\ y - y) (\ _ - id)
(==) = uRec (\ _ - Bool) isZero (\ _ - id)

I leave multiplication as an exercise.

The fact that these operators are commutative is
baked into their type.

To sum up, the fact that dependent types are good at
reflection makes them bad at parametricity, but there's
plenty of work in progress aimed at the kind of information
hiding which parametricity can then exploit.

There are good reasons to be optimistic here.

All the best

Conor

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Free theorems for dependent types?

[Eugene Kirpichov]

Hello,

Is there any research on applying free theorems / parametricity to
type systems more complex than System F; namely, Fomega, or calculus
of constructions and alike?

This seems very promising to me for the following reason: Take the
free theorem for 'sort::(a-a-Bool)-[a]-[a]'. The theorem could
possibly be a lot more powerful if there were a way to encode in the
type of 'sort' that it accepts a reflexive transitive antisymmetric
predicate, but the only way to express that is with dependent types.

Looks like the only thing one needs to add to System F is the
relational translation rule for a dependent product; but I haven't
tried doing it myself.

-- 
Eugene Kirpichov
Web IR developer, market.yandex.ru
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Free theorems for dependent types?

[Robin Green]

On Sun, 17 May 2009 23:10:12 +0400
Eugene Kirpichov ekirpic...@gmail.com wrote:

 Is there any research on applying free theorems / parametricity to
 type systems more complex than System F; namely, Fomega, or calculus
 of constructions and alike?

Yes. I did some research into it as part of my master's thesis, the
final version of which is not quite ready yet.

Basically, free theorems in the Calculus of Constructions can be
substantially more complicated, because they have to exclude certain
dependent types in order to be valid. So much so that I do not think
that they are necessarily worthwhile to use in proofs. But that is just
an intuition, and I have not done enough different kinds of proofs to
state this with any confidence.

-- 
Robin
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Free theorems for dependent types?

[Eugene Kirpichov]

I'm glad that someone is doing research in that direction!
Are your results so far applicable to create a free theorem for that
example with sortBy?

2009/5/17 Robin Green gree...@greenrd.org:
 On Sun, 17 May 2009 23:10:12 +0400
 Eugene Kirpichov ekirpic...@gmail.com wrote:

 Is there any research on applying free theorems / parametricity to
 type systems more complex than System F; namely, Fomega, or calculus
 of constructions and alike?

 Yes. I did some research into it as part of my master's thesis, the
 final version of which is not quite ready yet.

 Basically, free theorems in the Calculus of Constructions can be
 substantially more complicated, because they have to exclude certain
 dependent types in order to be valid. So much so that I do not think
 that they are necessarily worthwhile to use in proofs. But that is just
 an intuition, and I have not done enough different kinds of proofs to
 state this with any confidence.

 --
 Robin
 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe




-- 
Eugene Kirpichov
Web IR developer, market.yandex.ru
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Free theorems for dependent types?

[Joe Fredette]

This word has piqued my interest, I've hear it tossed around the 
community quite a bit, but never fully understood what it meant. What 
exactly is a 'free theorem'?


Eugene Kirpichov wrote:

Hello,

Is there any research on applying free theorems / parametricity to
type systems more complex than System F; namely, Fomega, or calculus
of constructions and alike?

This seems very promising to me for the following reason: Take the
free theorem for 'sort::(a-a-Bool)-[a]-[a]'. The theorem could
possibly be a lot more powerful if there were a way to encode in the
type of 'sort' that it accepts a reflexive transitive antisymmetric
predicate, but the only way to express that is with dependent types.

Looks like the only thing one needs to add to System F is the
relational translation rule for a dependent product; but I haven't
tried doing it myself.

  
begin:vcard
fn:Joseph Fredette
n:Fredette;Joseph
adr:Apartment #3;;6 Dean Street;Worcester;Massachusetts;01609;United States of America
email;internet:jfred...@gmail.com
tel;home:1-508-966-9889
tel;cell:1-508-254-9901
x-mozilla-html:FALSE
url:lowlymath.net, humbuggery.net
version:2.1
end:vcard

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Free theorems for dependent types?

[Ryan Ingram]

Free theorem's are theorems about functions that rely only on parametricity.

For example, consider any function f with the type
   forall a. a - a

From its type, I can tell you directly that this theorem holds:
  forall g :: A - B, x :: A,
  f (g  x) = g (f x)

(Note that the f on the left is B - B, the f on the right is A - A).

The term was popularized by Philip Wadler, in his paper Theorems for
Free! [1].  He noticed that many of the properties of functions that
one likes to prove come for free from their parametric type.  For
example, it's useful to know that

reverse (map fromEnum xs) == map fromEnum (reverse xs)

But this theorem comes for free from the type of reverse!  Given any

- f :: forall a. [a] - [a]
- g :: A - B
- xs :: [A]
we have the free theorem
- f (map g xs) = map g (f xs).

What this is saying is that any function (forall a. [a] - [a]) can't
do a whole lot; it can inspect the structure of the list it has been
given, and rearrange, duplicate, and/or remove some elements.  But the
output list can only contain elements from the input list, without
inspecting the elements themselves.

Therefore, if
f [1,2,3] == [1,1,2]
then
f abc == aab
and
f [True, True, False] == [True, True, True]
and
f [ [], [1], [1,2] ] == [ [], [], [1,2] ]
and so on.

Therefore mapping some pure function over the result can be done
before or after applying f; and we don't have to know *anything* about
f, aside from its type, to prove this.

  -- ryan

[1] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9875

On Sun, May 17, 2009 at 7:51 PM, Joe Fredette jfred...@gmail.com wrote:
 This word has piqued my interest, I've hear it tossed around the community
 quite a bit, but never fully understood what it meant. What exactly is a
 'free theorem'?

 Eugene Kirpichov wrote:

 Hello,

 Is there any research on applying free theorems / parametricity to
 type systems more complex than System F; namely, Fomega, or calculus
 of constructions and alike?

 This seems very promising to me for the following reason: Take the
 free theorem for 'sort::(a-a-Bool)-[a]-[a]'. The theorem could
 possibly be a lot more powerful if there were a way to encode in the
 type of 'sort' that it accepts a reflexive transitive antisymmetric
 predicate, but the only way to express that is with dependent types.

 Looks like the only thing one needs to add to System F is the
 relational translation rule for a dependent product; but I haven't
 tried doing it myself.



 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Learning GADT types to simulate dependent types

[Paul Johnson]

I'm trying to understand how to use GADT types to simulate dependent 
types.  I'm trying to write  a version of list that uses Peano numbers 
in the types to keep track of how many elements are in the list.  Like this:


{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}

module Plist where


infixr 3 :|

data Zero

data S a

class Add n1 n2 t | n1 n2 - t, n1 t - n2

instance Add Zero n n
instance Add (S n1) n2 (S t)

data Plist n a where
   Nil :: Plist Zero a
   (:|) :: a - Plist n a - Plist (S n) a

instance (Show a) = Show (Plist n a) where
   show Nil = Nil
   show (x :| xs) = show x ++  :|  ++ show xs

pHead :: Plist (S n) a - a
pHead (x :| _) = x

pTail :: Plist (S n) a - Plist n a
pTail (_ :| xs) = xs


pConcat Nil ys = ys
pConcat (x :| xs) ys = x :| pConcat xs ys


Everything works except the last function (pConcat).  I figured that it 
should add the lengths of its arguments together, so I created a class 
Add as shown in the Haskell Wiki at 
http://www.haskell.org/haskellwiki/Type_arithmetic.  But now I'm stuck.  
When I try to load this module I get:


Plist.hs:32:8:
   GADT pattern match in non-rigid context for `Nil'
 Tell GHC HQ if you'd like this to unify the context
   In the pattern: Nil
   In the definition of `pConcat': pConcat Nil ys = ys
Failed, modules loaded: none.

(Line 32 is pConcat Nil ys = ys)

So how do I do this?  Am I on the right track?  Can someone help improve 
my Oleg rating?


Thanks,

Paul.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Learning GADT types to simulate dependent types

[Daniel Fischer]

Am Samstag, 28. Juni 2008 19:51 schrieb Paul Johnson:
 I'm trying to understand how to use GADT types to simulate dependent
 types.  I'm trying to write  a version of list that uses Peano numbers
 in the types to keep track of how many elements are in the list.  Like
 this:

 {-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}

 module Plist where


 infixr 3 :|

 data Zero

 data S a

 class Add n1 n2 t | n1 n2 - t, n1 t - n2

 instance Add Zero n n
 instance Add (S n1) n2 (S t)

 data Plist n a where
 Nil :: Plist Zero a
 (:|) :: a - Plist n a - Plist (S n) a

 instance (Show a) = Show (Plist n a) where
 show Nil = Nil
 show (x :| xs) = show x ++  :|  ++ show xs

 pHead :: Plist (S n) a - a
 pHead (x :| _) = x

 pTail :: Plist (S n) a - Plist n a
 pTail (_ :| xs) = xs


 pConcat Nil ys = ys
 pConcat (x :| xs) ys = x :| pConcat xs ys


 Everything works except the last function (pConcat).  I figured that it
 should add the lengths of its arguments together, so I created a class
 Add as shown in the Haskell Wiki at
 http://www.haskell.org/haskellwiki/Type_arithmetic.  But now I'm stuck.
 When I try to load this module I get:

 Plist.hs:32:8:
 GADT pattern match in non-rigid context for `Nil'
   Tell GHC HQ if you'd like this to unify the context
 In the pattern: Nil
 In the definition of `pConcat': pConcat Nil ys = ys
 Failed, modules loaded: none.

 (Line 32 is pConcat Nil ys = ys)

 So how do I do this?  Am I on the right track?  Can someone help improve
 my Oleg rating?

 Thanks,

 Paul.


My Oleg rating isn't high either, and certainly you can do it more elegant, 
but


class Concat l1 l2 l3 | l1 l2 - l3, l1 l3 - l2 where
pConcat :: l1 a - l2 a - l3 a

instance Concat (Plist Zero) (Plist n) (Plist n) where
pConcat _ ys = ys

instance Concat (Plist n1) (Plist n2) (Plist t) =
Concat (Plist (S n1)) (Plist n2) (Plist (S t)) where
pConcat (x :| xs) ys = x :| pConcat xs ys


works, you don't even need the Add class then - btw, you'd want
instance Add n1 n2 t = Add (S n1) n2 (S t)
anyway.

Cheers,
Daniel
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Learning GADT types to simulate dependent types

[Dan Doel]

On Saturday 28 June 2008, Paul Johnson wrote:
 I'm trying to understand how to use GADT types to simulate dependent
 types.  I'm trying to write  a version of list that uses Peano numbers
 in the types to keep track of how many elements are in the list.  Like
 this:

 {-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}

 module Plist where


 infixr 3 :|

 data Zero

 data S a

 class Add n1 n2 t | n1 n2 - t, n1 t - n2

 instance Add Zero n n
 instance Add (S n1) n2 (S t)

 data Plist n a where
 Nil :: Plist Zero a
 (:|) :: a - Plist n a - Plist (S n) a

 instance (Show a) = Show (Plist n a) where
 show Nil = Nil
 show (x :| xs) = show x ++  :|  ++ show xs

 pHead :: Plist (S n) a - a
 pHead (x :| _) = x

 pTail :: Plist (S n) a - Plist n a
 pTail (_ :| xs) = xs


 pConcat Nil ys = ys
 pConcat (x :| xs) ys = x :| pConcat xs ys


 Everything works except the last function (pConcat).  I figured that it
 should add the lengths of its arguments together, so I created a class
 Add as shown in the Haskell Wiki at
 http://www.haskell.org/haskellwiki/Type_arithmetic.  But now I'm stuck.
 When I try to load this module I get:

 Plist.hs:32:8:
 GADT pattern match in non-rigid context for `Nil'
   Tell GHC HQ if you'd like this to unify the context
 In the pattern: Nil
 In the definition of `pConcat': pConcat Nil ys = ys
 Failed, modules loaded: none.

 (Line 32 is pConcat Nil ys = ys)

 So how do I do this?  Am I on the right track?  Can someone help improve
 my Oleg rating?

There are a couple issues that jump out at me. First, your second instance for 
Add is a bit off. It should be more like:

instance (Add n1 n2 t) = Add (S n1) n2 (S t)

Second, the reason you're getting that particular error with pConcat is that 
it doesn't have a type signature. Matching on GADTs requires one. However, 
fixing those here, I still got errors, and I'm not enough of a type 
class/fundep wizard to know what the problem is. Instead, I might suggest 
using type families for the type-level arithmetic:

type family Add n1 n2 :: *
type instance Add Zero   n2 = n2
type instance Add (S n1) n2 = S (Add n1 n2)

Then the signature of pConcat becomes:

pConcat :: Plist m a - Plist n a - Plist (Add m n) a

Which works fine. As an added bonus, the type family doesn't require 
undecidable instances like the type class does.

Type families are a bit iffy in 6.8.*, but they'll work all right for simple 
stuff like this, at least.

Cheers,
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Learning GADT types to simulate dependent types

[Paul Johnson]

Daniel Fischer wrote:


My Oleg rating isn't high either, and certainly you can do it more elegant, 
but



class Concat l1 l2 l3 | l1 l2 - l3, l1 l3 - l2 where
pConcat :: l1 a - l2 a - l3 a

instance Concat (Plist Zero) (Plist n) (Plist n) where
pConcat _ ys = ys

instance Concat (Plist n1) (Plist n2) (Plist t) =
Concat (Plist (S n1)) (Plist n2) (Plist (S t)) where
pConcat (x :| xs) ys = x :| pConcat xs ys


works, you don't even need the Add class then - btw, you'd want
instance Add n1 n2 t = Add (S n1) n2 (S t)
anyway.

  
Thanks, and also thanks to Dan Doel who showed how to do it with the new 
type families.  I'll stick with the Fundeps solution here for the moment 
until type families settle down, but that method is cleaner. 


I was also able to write this:


class Concat p1 p2 p3 | p1 p2 - p3, p1 p3 - p2 where
   pConcat :: p1 a - p2 a - p3 a
   pBogus :: p1 a - p2 a - p3 a

instance Concat (Plist Zero) (Plist n) (Plist n) where
   pConcat _ ys = ys
   pBogus _ ys = ys

instance Concat (Plist n1) (Plist n2) (Plist t) =
   Concat (Plist (S n1)) (Plist n2) (Plist (S t)) where
   pConcat (x :| xs) ys = x :| pConcat xs ys
   pBogus xs ys = ys

And indeed the second definition of pBogus gave me a compile-time type 
error because the length of the result didn't agree with the type length.


I'm going to be doing a presentation on Haskell for my boss soon, and 
this should definitely impress (he has a solid coding background).


Thanks again,

Paul.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] ANNOUNCE: parameterized-data 0.1 - Parameterized data library implementing lightweight dependent types

[Alfonso Acosta]

 This library provides an implementation of parameterized types using
type-level computations to implement the type parameters and emulate
dependent types.

 Right now only fixed-sized vectors are provided (based on Oleg's
Number-parameterized types [1]  and Frederik Eaton's Vectro library
[2])

HackageDB page:
http://hackage.haskell.org/cgi-bin/hackage-scripts/package/parameterized-data-0.1

Darcs repository: http://code.haskell.org/parameterized-data/

Again, big thanks to Oleg and Wolfgang for their help and suggestions.

[1] http://okmij.org/ftp/Haskell/number-parameterized-types.html
[2] http://ofb.net/~frederik/vectro/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: How do I simulate dependent types using phantom types?

[Bertram Felgenhauer]

DavidA wrote:
 Twan van Laarhoven twanvl at gmail.com writes:
  The solution is to use a dummy parameter:
class IntegerType a where
value :: a - Integer
 
 Thanks to all respondents for this suggestion. That works great.

I prefer a slightly elaborate way,

 newtype Mark n t = Mark t

 -- provide conversion from and to dummy functions because they are
 -- much more convenient to use.
 toDummy :: Mark n t - n - t
 toDummy (Mark x) _ = x

 fromDummy :: (n - t) - Mark n t
 fromDummy f = Mark (f undefined)

 class Natural a where
value' :: Mark a Integer

 value :: Natural a = a - Integer
 value = toDummy value'

The advantage of this approach is that the 'Natural' class dictionary
contains a constant Integer value, not some function that the compiler
doesn't know anything about. This makes no difference for simple uses,
but once you define type level natural numbers, like

 dataZero = Zero
 newtype D0 a = D0 a
 newtype D1 a = D1 a

with instances,

 instance Natural Zero where
 value' = Mark 0

 instance Natural a = Natural (D0 a) where
 value' = fromDummy (\(D0 d) - value d * 2)

 instance Natural a = Natural (D1 a) where
 value' = fromDummy (\(D1 d) - value d * 2 + 1)

you get an actual speedup at runtime, because the value represented by
the type is passed directly in the class dictionary and doesn't have to
be recomputed each time value is called. (Note: it *is* possible to
share intermediate results even with dummy functions, but I got a
significant speed boost in my modular arithmetic code with this
trick anyway.)

This also opens up a *naughty* way to construct such phantom types in
GHC. When I say naughty I mean it - use this code at your own risk.

 -- Or is this reify? I'm confused about the convention here.
 reflect :: Integer - (forall n . Nat n = Mark n a) - a
 reflect = flip unsafeCoerce

which can be used like this:

*Test reflect 42 value'
42
*Test reflect 7 (fromDummy (\d - value d * 6))
42

It is an interesting exercise to implement

  reflect :: Integer - (forall n . Nat n = Mark n a) - a

using Zero, D0 and D1 :)

Bertram
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] How do I simulate dependent types using phantom types?

[DavidA]

Hi,

I am trying to implement quadratic fields Q(sqrt d). These are numbers of the 
form a + b sqrt d, where a and b are rationals, and d is an integer.

In an earlier attempt, I tried
data QF = QF Integer Rational Rational
(see http://www.polyomino.f2s.com/david/haskell/hs/QuadraticField.hs.txt)
The problem with this approach is that it's not really type-safe:
I can attempt to add a + b sqrt 2 to c + d sqrt 3, whereas this should be a 
type error because 2 /= 3.

So I thought I'd have a go at doing it with phantom types. In effect I'd be 
using phantom types to simulate dependent types. Here's the code:

{-# OPTIONS_GHC -fglasgow-exts #-}

import Data.Ratio

class IntegerType a where
value :: Integer

data Two
instance IntegerType Two where value = 2

data Three
instance IntegerType Three where value = 3

data QF d = QF Rational Rational deriving (Eq)

instance IntegerType d = Show (QF d) where
show (QF a b) = show a ++  +  ++ show b ++  sqrt  ++ show value

instance IntegerType d = Num (QF d) where
QF a b + QF a' b' = QF (a+a') (b+b')
negate (QF a b) = QF (-a) (-b)
QF a b * QF c d = QF (a*c + b*d*value) (a*d + b*c)
fromInteger n = QF (fromInteger n) 0

The problem is, this doesn't work. GHC complains:
The class method `value'
mentions none of the type variables of the class IntegerType a
When checking the class method: value :: Integer
In the class declaration for `IntegerType'

Is what I'm trying to do reasonable? If no, what should I be doing instead? If 
yes, why doesn't GHC like it?

Thanks, David

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] How do I simulate dependent types using phantom types?

[Lennart Augustsson]

Use
  value :: a - Integer


On 8/18/07, DavidA [EMAIL PROTECTED] wrote:

 Hi,

 I am trying to implement quadratic fields Q(sqrt d). These are numbers of
 the
 form a + b sqrt d, where a and b are rationals, and d is an integer.

 In an earlier attempt, I tried
 data QF = QF Integer Rational Rational
 (see http://www.polyomino.f2s.com/david/haskell/hs/QuadraticField.hs.txt)
 The problem with this approach is that it's not really type-safe:
 I can attempt to add a + b sqrt 2 to c + d sqrt 3, whereas this should be
 a
 type error because 2 /= 3.

 So I thought I'd have a go at doing it with phantom types. In effect I'd
 be
 using phantom types to simulate dependent types. Here's the code:

 {-# OPTIONS_GHC -fglasgow-exts #-}

 import Data.Ratio

 class IntegerType a where
 value :: Integer

 data Two
 instance IntegerType Two where value = 2

 data Three
 instance IntegerType Three where value = 3

 data QF d = QF Rational Rational deriving (Eq)

 instance IntegerType d = Show (QF d) where
 show (QF a b) = show a ++  +  ++ show b ++  sqrt  ++ show value

 instance IntegerType d = Num (QF d) where
 QF a b + QF a' b' = QF (a+a') (b+b')
 negate (QF a b) = QF (-a) (-b)
 QF a b * QF c d = QF (a*c + b*d*value) (a*d + b*c)
 fromInteger n = QF (fromInteger n) 0

 The problem is, this doesn't work. GHC complains:
 The class method `value'
 mentions none of the type variables of the class IntegerType a
 When checking the class method: value :: Integer
 In the class declaration for `IntegerType'

 Is what I'm trying to do reasonable? If no, what should I be doing
 instead? If
 yes, why doesn't GHC like it?

 Thanks, David

 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] How do I simulate dependent types using phantom types?

[Twan van Laarhoven]

DavidA wrote:


Hi,

I am trying to implement quadratic fields Q(sqrt d). These are numbers of the 
form a + b sqrt d, where a and b are rationals, and d is an integer.


...

class IntegerType a where
value :: Integer

The problem is, this doesn't work. GHC complains:
The class method `value'
mentions none of the type variables of the class IntegerType a
When checking the class method: value :: Integer
In the class declaration for `IntegerType'

Is what I'm trying to do reasonable? If no, what should I be doing instead? If 
yes, why doesn't GHC like it?


You are on the right track. The problem with the class method is that it 
doesn't use type 'a' anywhere, consider

 f :: Integer
 f = value
What class instance should be used here?

The solution is to use a dummy parameter:
 class IntegerType a where
 value :: a - Integer
And call it like:
 f = value (undefined :: Two)

So for instance:
 instance IntegerType d = Show (QF d) where
 show (QF a b) = show a ++  +  ++ show b ++  sqrt 
   ++ show (value (undefined::d))

The problem is that this doesn't work, because d is not in scope, you 
need the scoped type variables extension:


 valueOfQF :: forall a. IntegerType a = QF a - Integer
 valueOfQF qf = value (undefined :: a)

or maybe better, change the class:

 class IntegerType a where
 value :: QF a - Integer

Now you can simply use

 instance IntegerType d = Show (QF d) where
 show qf@(QF a b) = show a ++  +  ++ show b ++  sqrt 
 ++ show (value qf)

Twan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: How do I simulate dependent types using phantom types?

[DavidA]

Twan van Laarhoven twanvl at gmail.com writes:

 The solution is to use a dummy parameter:
   class IntegerType a where
   value :: a - Integer
 And call it like:
   f = value (undefined :: Two)
 
 So for instance:
   instance IntegerType d = Show (QF d) where
   show (QF a b) = show a ++  +  ++ show b ++  sqrt 
 ++ show (value (undefined::d))

Thanks to all respondents for this suggestion. That works great.

 
 The problem is that this doesn't work, because d is not in scope, you 
 need the scoped type variables extension:
 
   valueOfQF :: forall a. IntegerType a = QF a - Integer
   valueOfQF qf = value (undefined :: a)

Well actually, your first attempt *did* work for me (using GHC 6.6.1). Is this 
not behaviour that I can rely on?

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell] (Succ Haskell') `and` $ dependent types

[Vivian McPhail]

Hello,

As the authors point out [1], coal-face time needs to be expended before
real world adoption of Dependently-Typed functional programming.  But let's
get the ball rolling.  They say that haskell programmers are normally averse
to dependent types.  Is this true?  It seems to me that one of the appeals
of Haskell is the ability to program in a prove perfect, write once
(elegant) style.  Is not dependent typing a good move towards this goal?.
It addresses a problem [2] with which we, in our everyday common
inter-hominem usage, can deal -- with which (ideal) Haskell should deal.

While the major Haskell implementations would require a substantial
overhaul, the change at the syntactic level appears to be minimal.  There
also needs to be advance with respect to programmer development (automatic
edit-time inference of (some) types). What are peoples' thoughts on adding
dependent types to haskell as a non-incremental evolutionary step?  Does the
haskell community want to stick with conservative additions to Haskell and a
static base, or does the haskell community want to stay in step with the
best theoretical developments?

Vivian

[1] http://www.informatik.uni-bonn.de/~loeh/LambdaPi.html
[2] http://thread.gmane.org/gmane.comp.lang.haskell.cafe/21314
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Re: (Succ Haskell') `and` $ dependent types

[Stefan O'Rear]

On Sun, Jul 15, 2007 at 09:04:16AM +1200, Vivian McPhail wrote:
 Hello,

 As the authors point out [1], coal-face time needs to be expended before
 real world adoption of Dependently-Typed functional programming.  But let's
 get the ball rolling.  They say that haskell programmers are normally 
 averse
 to dependent types.  Is this true?  It seems to me that one of the appeals
 of Haskell is the ability to program in a prove perfect, write once
 (elegant) style.  Is not dependent typing a good move towards this goal?.
 It addresses a problem [2] with which we, in our everyday common
 inter-hominem usage, can deal -- with which (ideal) Haskell should deal.

 While the major Haskell implementations would require a substantial
 overhaul, the change at the syntactic level appears to be minimal.  There
 also needs to be advance with respect to programmer development (automatic
 edit-time inference of (some) types). What are peoples' thoughts on adding
 dependent types to haskell as a non-incremental evolutionary step?  Does 
 the
 haskell community want to stick with conservative additions to Haskell and 
 a
 static base, or does the haskell community want to stay in step with the
 best theoretical developments?

 Vivian

 [1] http://www.informatik.uni-bonn.de/~loeh/LambdaPi.html
 [2] http://thread.gmane.org/gmane.comp.lang.haskell.cafe/21314

Dependant types aren't new, they're ten times older than Haskell ;)

I don't even think that adding dependant types to Haskell would be that
hard.  Most of the needed infrastructure (notably the binder rule,
lexically scoped type variables, and explicit instantiation) already
exists in the implementation of rank-N types in GHC.  I think much of
the work would be in revising Core (currently it uses a variant of
Barandregt's λω, which is strictly less powerful (IIUC) than the full
dependant λC) and flattening the typeinfer/kindinfer staging.

Of course, since Haskell is not strongly normalizing, we would not be
able to use a calculus where applications of CONV are implicit.

Interaction with qualified types (type classes, MPTC, fundeps, implicit
parameters, extensible records, associated type synonym equality
predicates, etc) could be interesting, in both senses of the word.

Stefan


signature.asc
Description: Digital signature
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: (Succ Haskell') `and` $ dependent types

[Stefan O'Rear]

On Sun, Jul 15, 2007 at 09:04:16AM +1200, Vivian McPhail wrote:
 Hello,

 As the authors point out [1], coal-face time needs to be expended before
 real world adoption of Dependently-Typed functional programming.  But let's
 get the ball rolling.  They say that haskell programmers are normally 
 averse
 to dependent types.  Is this true?  It seems to me that one of the appeals
 of Haskell is the ability to program in a prove perfect, write once
 (elegant) style.  Is not dependent typing a good move towards this goal?.
 It addresses a problem [2] with which we, in our everyday common
 inter-hominem usage, can deal -- with which (ideal) Haskell should deal.

 While the major Haskell implementations would require a substantial
 overhaul, the change at the syntactic level appears to be minimal.  There
 also needs to be advance with respect to programmer development (automatic
 edit-time inference of (some) types). What are peoples' thoughts on adding
 dependent types to haskell as a non-incremental evolutionary step?  Does 
 the
 haskell community want to stick with conservative additions to Haskell and 
 a
 static base, or does the haskell community want to stay in step with the
 best theoretical developments?

 Vivian

 [1] http://www.informatik.uni-bonn.de/~loeh/LambdaPi.html
 [2] http://thread.gmane.org/gmane.comp.lang.haskell.cafe/21314

Dependant types aren't new, they're ten times older than Haskell ;)

I don't even think that adding dependant types to Haskell would be that
hard.  Most of the needed infrastructure (notably the binder rule,
lexically scoped type variables, and explicit instantiation) already
exists in the implementation of rank-N types in GHC.  I think much of
the work would be in revising Core (currently it uses a variant of
Barandregt's λω, which is strictly less powerful (IIUC) than the full
dependant λC) and flattening the typeinfer/kindinfer staging.

Of course, since Haskell is not strongly normalizing, we would not be
able to use a calculus where applications of CONV are implicit.

Interaction with qualified types (type classes, MPTC, fundeps, implicit
parameters, extensible records, associated type synonym equality
predicates, etc) could be interesting, in both senses of the word.

Stefan


signature.asc
Description: Digital signature
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime

[Haskell-cafe] An example of dependent types [was: Simple GADT parser for the eval example]

[oleg]

Greg Buchholz has posed an interesting problem of writing a
typechecker. Given untyped terms of the form

 data Expr = ELit Int
   | EInc Expr
   | EIsZ Expr


we are to compute typed terms:

 data Term a where
 Lit  :: Int - Term Int
 Inc  :: Term Int - Term Int
 IsZ  :: Term Int - Term Bool

That is, we need to write a function 

   typecheck :: Expr - Term a

Actually, Greg Buchholz posed a simpler example, of a function my_read
   my_read :: Expr - Term a

Although it has the same signature, the intent is different. When the
user writes my_read exp, the user is supposed to *specify* the type
of the desired result. Just as when we write read 1, we are supposed
to specify the type of the expected value: Int, Integer, etc. The
function typecheck has a different intent: it *computes* the result
type. It is indeed the typechecker: given the expression, we 
compute its type -- or report a failure if the expression is
ill-typed. That is, the result *type* Term a is a function of the
*value* Expr. Thus is truly a problem of dependent types. And Haskell
is up to it: Haskell is genuinely a dependently typed language.

We show the solution that uses no GADTs and no representation types.
We retain however the eval function in the previous message that uses
GADT. Our solution uses type classes. It seems to some the
type-checking rules stated as instances of the TypeCheck class take a
particular natural form. Indeed:

 -- given term e, compute its type t
 class TypeCheck e t | e - t where
 typecheck :: e - Term t

 instance TypeCheck FLit Int where
 typecheck (FLit x) = Lit x

 instance TypeCheck e Int = TypeCheck (FInc e) Int where
 typecheck (FInc e) = Inc (typecheck e)

 instance TypeCheck e Int = TypeCheck (FIsZ e) Bool where
 typecheck (FIsZ e) = IsZ (typecheck e)

 instance (TypeCheck e1 Bool, TypeCheck e2 t, TypeCheck e3 t) 
 = TypeCheck (FIf e1 e2 e3) t where
 typecheck (FIf e1 e2 e3) = If (typecheck e1) (typecheck e2)(typecheck e3)

 instance (TypeCheck e1 t1, TypeCheck e2 t2) 
 = TypeCheck (FPair e1 e2) (t1,t2) where
 typecheck (FPair e1 e2) = Pair (typecheck e1) (typecheck e2)

 instance TypeCheck e (t1,t2) = TypeCheck (FFst e) t1 where
 typecheck (FFst e) = Fst (typecheck e)

 instance TypeCheck e (t1,t2) = TypeCheck (FSnd e) t2 where
 typecheck (FSnd e) = Snd (typecheck e)


In the paper, the IsZ rule would have been written as
|- e : int
   ---
|- IsZ e : bool

(We don't need the environment Gamma as our language has no
variables). I submit the typeclass notation takes less space. 

The typechecking rules above operate on `lifted' terms: FLit, FInc,
etc:

 newtype FLit = FLit Int
 newtype FInc e = FInc e
 newtype FIsZ e = FIsZ e

rather than the original terms Exp. The conversion is straightforward,
via Template Haskell:

 type F = Q TH.Exp
 parse :: Expr - F
 parse (ELit x) = [e| FLit $(litE . integerL . fromIntegral $ x) |]
 parse (EInc x) = [e| FInc $(parse x) |]
 parse (EIsZ x) = [e| FIsZ $(parse x) |]

The only inconvenience of using the Template Haskell is the necessity
of splitting the whole code into two modules.

we can then write:

 e1 = EIf (ELit 1) (ELit 2) (ELit 3)
 e2 = (EIf (EIsZ (ELit 0))   ++
   (EInc (ELit 1))   ++
   (EFst (EPair (ELit 42)++
(ELit 43

 t1' = $(parse . read $ e1)
 t2' = $(parse . read $ e2)

*G :t t1'
t1' :: FIf FLit FLit FLit
*G :t t2'
t2' :: FIf (FIsZ FLit) (FInc FLit) (FFst (FPair FLit FLit))

 -- Causes the typechecking error: cannot match Int against the Bool
 -- tt1 = typecheck t1'
 tt2 = typecheck t2'

*G :t tt2
tt2 :: Term Int

Obviously, e1 is ill-formed and so cannot be typechecked. The term e2
is well-typed, and the typechecker has figured out its type, which is
Term Int. There was no need for any type annotation.

The term tt2 can then be evaluated.

The code: file GP.hs
{-# OPTIONS -fglasgow-exts #-}

module GP where

import Language.Haskell.TH hiding (Exp)
import qualified Language.Haskell.TH as TH (Exp)
import Language.Haskell.TH.Ppr

-- untyped terms, at Level 0
data Expr = ELit Int
  | EInc Expr
  | EIsZ Expr
  | EPair Expr Expr
  | EIf Expr Expr Expr
  | EFst Expr
  | ESnd Expr
deriving (Read,Show)

-- Untyped terms, at Level 1
type F = Q TH.Exp
newtype FLit = FLit Int
newtype FInc e = FInc e
newtype FIsZ e = FIsZ e
data FPair e1 e2 = FPair e1 e2
data FIf e1 e2 e3 = FIf e1 e2 e3
newtype FFst e = FFst e
newtype FSnd e = FSnd e

parse :: Expr - F
parse (ELit x) = [e| FLit $(litE . integerL . fromIntegral $ x) |]
parse (EInc x) = [e| FInc $(parse x) |]
parse (EIsZ x) = [e| FIsZ $(parse x) |]
parse (EFst x) = [e| FFst $(parse x) |]
parse (ESnd x) = [e| FSnd $(parse x) |]
parse (EPair x y) = [e| FPair $(parse x) $(parse y) |]
parse (EIf x y z) = [e| FIf $(parse x) $(parse y

[Haskell-cafe] Re: An example of dependent types [was: Simple GADT parser for the eval example]

[Greg Buchholz]

[EMAIL PROTECTED] wrote:
 
 Greg Buchholz has posed an interesting problem of writing a
 typechecker. Given untyped terms of the form

...snip...

 We show the solution that uses no GADTs and no representation types.
 We retain however the eval function in the previous message that uses
 GADT. Our solution uses type classes. It seems to some the
 type-checking rules stated as instances of the TypeCheck class take a
 particular natural form.

...snip...

 
 rather than the original terms Exp. The conversion is straightforward,
 via Template Haskell:
 
  type F = Q TH.Exp
  parse :: Expr - F
  parse (ELit x) = [e| FLit $(litE . integerL . fromIntegral $ x) |]
  parse (EInc x) = [e| FInc $(parse x) |]
  parse (EIsZ x) = [e| FIsZ $(parse x) |]
  
  t1' = $(parse . read $ e1)
  t2' = $(parse . read $ e2)
 
 *G :t t1'
 t1' :: FIf FLit FLit FLit
 *G :t t2'
 t2' :: FIf (FIsZ FLit) (FInc FLit) (FFst (FPair FLit FLit))

Nice.  But using TH means we have to know everthing about the
strings we want to evaluate at compile time right?  So you can't do
something like...

main = do l - getLine
  print $ (eval.typecheck) ($(parse . read $ l))

...right? (Even if you can get around GHC complaining about a 'stage
restriction').  Whereas, it would be possible with with the my_read
and other versions.  Anyway, as long as we're going down that route, we
might as well get rid of the GADTs and go for a pure type class version
of eval... 

http://lambda-the-ultimate.org/node/1787 

...(great minds think alike, right? ;-)  I guess I should have mentioned
that thread in my first message.

Thanks,

Greg Buchholz


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell] Eliminating Multiple-Array Bound Checking through Non-dependent types

[oleg]

An earlier message showed an example of writing code with non-trivial
static guarantees in the present-day Haskell (i.e., Haskell98 + rank-2
types).

http://pobox.com/~oleg/ftp/Haskell/types.html#branding

Although this approach obviously falls short of the genuine dependent
typing, we can use it in the existing, well-maintained functional
language systems. Thus we may begin to acquire taste for dependent
typing -- which, McBride at al. point out, matter.

The present message shows a more advanced example -- eliminating array
bound checking when processing several arrays at a time. The number of
arrays to process is not statically known. Furthermore, the arrays may
have different sizes and bounds -- potentially, empty and
non-overlapping bounds. The example involves native Haskell arrays,
index computations, and general recursion. All array indexing
operations are statically guaranteed to be safe -- and so we can
safely use an efficient unsafeAt provided by GHC seemingly for that
purpose. The code is efficient; the static assurances in the main loop
over arrays cost us no run-time overhead. The example uses only
Haskell98 + higher-ranked types. No new type classes are
introduced. The safety is based on: Haskell type system, quantified
type variables, and a compact general-purpose trusted kernel.
I thank Daniel Yokomizo for the challenge.

Our example is folding over multiple, variously-sized arrays.  This
is like a fold over an array -- generalized to an arbitrary number of
arrays, whose index ranges do not have to be the same (and do not have
to overlap). Typing this example in a genuinely dependent type system
is probably going to be quite challenging.

Our goal is to implement a function

 marray_fold :: (Ix i, Integral i) =
 (seed - [e] - seed) - seed - [Array i e] - seed

Its third argument is a list of arrays; the arrays have all the same
element and index types; the actual sizes (that is, the lower and
upper bounds) may differ. Some arrays in the list may even be empty
(with the lower bound higher than the upper one). The function
marray_fold, like left fold, applies its left argument to the
values extracted from the corresponding arrays. Because arrays may
have different sizes and bounds, marray_fold operates over the range
of indices that is the intersection of the ranges of the argument
arrays.

For example:

  dot a1 a2 = marray_fold (\seed l - product l + seed) 0 [a1,a2]

computes the dot products of two arrays. 

Granted our example is a bit contrived: in practice one would probably
use ``fixed arity'' multiple array fold (similar to zipWith, zipWith3,
etc -- which are more efficient and simpler to implement).  Also
simple is the processing of arrays of the same bounds (and invoking an
error continuations if the bounds turn out different).  OTH, our
present example is more challenging and thus more interesting.

Here's the complete implementation (assuming the short trusted
branding library explained below).


 {-# OPTIONS -fglasgow-exts #-}
 module MDep where
 import Data.Array

 marray_fold :: (Ix i, Integral i) =
(seed - [e] - seed) - seed - [Array i e] - seed
 marray_fold _ seed [] = seed  -- No arrays, no fold
 marray_fold f seed arrs = brands arrs (marray_fold' f seed) seed

 marray_fold' f seed (barrs, bl, bh) = loop (bl2i bl) seed
   where loop bi seed = bsucc bh bi (\bi' - loop bi' seed') seed'
  where seed' = f seed (map (!. bi) barrs)
  
 brands :: (Ix i, Integral i) = [Array i e]
   - (forall s. ([BArray s i e], BLow s i, BHi s i) - w)
   - w - w
 brands [arr] consumer onempty =
 brand arr (\ (barr,bl,bh) - consumer ([barr],bl,bh)) onempty
 brands (a:arrs) consumer onempty =
 brands arrs (\bbars - brand_merge bbars a consumer onempty) onempty

The function |brands| computes the intersection index range for the
given arrays, and brands each array and the intersection range. The
range is given as a pair (BLow s i, BHi s i). The quantified (and thus
unforgeable) type variable |s| represents the brand. The function
|brands| has a higher-ranked type and must have a
signature. Incidentally, functions like that are relatively rare;
processors of the list of arrays of the same brand do not require any
signature (cf. marray_fold').

The folding loop has as few index comparison operations as
algorithmically needed, i.e., only one per iteration. Operator (!.) is
a statically safe array indexing operator. The type system and the
trust properties of the kernel below guarantee that in the expression
arr !. m the index `m' is positively in range of the array `arr'
bounds. 

Here are a few test cases, of the dot product over several arrays

 dots ars = marray_fold (\seed l - product l + seed) 0 ars
 test1 = dots [listArray (1,5) [1..]]
 test2 = dots [listArray (1,5) [1..],listArray (1,5) [1,1..]]
 test3 = dots [listArray (1,5) [1..],listArray (5,1) [1,1..]]
 test4 = dots [listArray (1,5) 

Re: [Haskell] Dependent types, was:2-D Plots, graphical representation of massive data

[MR K P SCHUPKE]

I think you are confusing Dependent Types with Functional Dependencies.

Actually the two are not that dissimilar... If we allow types to depend
on types (which is what Functional Dependencies allow) IE:

class a b | a - b
instance Int Float
instance Float Int

For example is really a function on the type level mapping a to b. All
that is missing is a way to make types depend on values... which can
be done with dictionary passing. Here is an example:

class ReifyBool t w where
reifyBool :: Prelude.Bool - t - w
instance (Apply t AllTrue w,Apply t AllFalse w) = ReifyBool t w where
reifyBool Prelude.True t = apply t AllTrue
reifyBool Prelude.False t = apply t AllFalse

The limitation here is that an 'instance' must exist for each possibility
in the program, so we are limited to a finite range of values... although
we can use type recursion in the class to make the code smaller, we still
must have some limit known at compile time, for example Int:

class (NotNegative m,NotPositive n) = ReifyNotPositive m t i n w where
reifyNotPositive :: Integral i = m - t - i - n - w
instance NotPositive n = ReifyNotPositive Zero t i n w where
reifyNotPositive _ _ _ _ = error Number to be reified exceeds maximum range.
instance (NotPositive n,ReifyNotPositive m t i (Pre n) w,Ctrl.Apply t n w)
= ReifyNotPositive (Suc m) t i n w where
reifyNotPositive (Suc m) t i n
| i0 = reifyNotPositive m t (i+1) (Pre n)
| otherwise = Ctrl.apply t n

(I appologise if the code is a little verbose, but to avoid mistakes I have
cut and pasted from a working project - but you can see the important
features)...

So by combining reification to a type level representation and functional
dependancies we arrive at dependant types...

Keean./
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Dependent types, was:2-D Plots, graphical representation of massive data

[Tomasz Zielonka]

On Fri, Aug 27, 2004 at 10:26:51AM -0400, Michael Manti wrote:
 I recognize that I'm far out of my depth here--both in Haskell and in
 mathematics--but I'll ask anyway. In what ways are dependent types
 (http://haskell.org/hawiki/FunDeps,
 http://www.cse.ogi.edu/~mpj/pubs/fundeps.html) insufficient to address
 these issues? 

I think you are confusing Dependent Types with Functional Dependencies.
They are two completely different things. The former means a type system
in which types can depend on values, the latter (in context of type
systems) is an extension of type classes which allows to eliminate
unnecessary ambiguities.

Best regards,
Tom

-- 
.signature: Too many levels of symbolic links
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

RE: [Haskell] Dependent types, was:2-D Plots, graphical representation of massive data

[Jacques Carette]

 I think Jacques possibly means the ability to do static checking of matrix
 and vector extents, to make sure that you don't try to perform operations
 like matrix-vector multiply on operands whose extents do not match. If you
 want to have this ability on your language, then you will have to restrict
 the way you are allowed to construct array bounds so the equations that
 arise can be solved. Possibly a dependent type system can be helpful for
 this.

This is indeed what I meant.

If one is going to move from a dynamically typed language (like Matlab,
Maple, Mathematica, etc) to something statically typed, then the expectation
is that this is going to truly help.  And, for many applications, it does
[this is partly why I have an MSc student coding a reverse engineering
application in Haskell].

Since the claim of static typing is that things cannot go wrong at run-time,
one start to think (incorrectly, but optimistically) that this means that
'nonsense' cannot happen at run-time.  And multiplying matricies with
non-matching sizes is nonsense, so it is rather disappointing that, without
tricks, this is not caught at compilation time.

Matrix length are one of many commonly occuring dependent types in
mathematics.  Variable names for polynomials, expansion point and 'scale'
for generalized series expansions, coefficient ring for normalization and
factorization of polynomials, and so on up the food chain.  The dependencies
get quite interesting when one is dealing with modelling mixed PDEs and
recurrence equations as ideals in rings of Ore polynomials!  

Jacques

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

RE: [Haskell] Dependent types, was:2-D Plots, graphical representation of massive data

[Michael Manti]

I recognize that I'm far out of my depth here--both in Haskell and in mathematics--but 
I'll ask anyway. In what ways are dependent types (http://haskell.org/hawiki/FunDeps, 
http://www.cse.ogi.edu/~mpj/pubs/fundeps.html) insufficient to address these issues? 
 
On Friday, August 27, 2004, at 10:04AM, Jacques Carette [EMAIL PROTECTED] wrote:

 I think Jacques possibly means the ability to do static checking of matrix
 and vector extents, to make sure that you don't try to perform operations
 like matrix-vector multiply on operands whose extents do not match. If you
 want to have this ability on your language, then you will have to restrict
 the way you are allowed to construct array bounds so the equations that
 arise can be solved. Possibly a dependent type system can be helpful for
 this.

This is indeed what I meant.

If one is going to move from a dynamically typed language (like Matlab,
Maple, Mathematica, etc) to something statically typed, then the expectation
is that this is going to truly help.  And, for many applications, it does
[this is partly why I have an MSc student coding a reverse engineering
application in Haskell].

Since the claim of static typing is that things cannot go wrong at run-time,
one start to think (incorrectly, but optimistically) that this means that
'nonsense' cannot happen at run-time.  And multiplying matricies with
non-matching sizes is nonsense, so it is rather disappointing that, without
tricks, this is not caught at compilation time.

Matrix length are one of many commonly occuring dependent types in
mathematics.  Variable names for polynomials, expansion point and 'scale'
for generalized series expansions, coefficient ring for normalization and
factorization of polynomials, and so on up the food chain.  The dependencies
get quite interesting when one is dealing with modelling mixed PDEs and
recurrence equations as ideals in rings of Ore polynomials!  

Jacques

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell




Michael Manti
[EMAIL PROTECTED]
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Re: Dependent Types in Haskell

[oleg]

Martin Sulzmann stated the goal of the append exercise as follows:

] Each list carries now some information about its length.
] The type annotation states that the sum of the output list
] is the sum of the two input lists.

I'd like to give a Haskell implementation of such an append
function, which makes an extensive use of partial signatures and, in
generally, relies on the compiler to figure out the rest of the
constraints. We also separate the skeleton of the list from the type
of the list elements.

This solution differs from the Haskell solution append3.hs given in
Martin Sulzmann's message. The latter solution relies on the trusted
kernel: the equality datatype E. It is quite easy to subvert
append3.hs if we set up E with particular run-time values. The error
will not be discovered statically -- nor dynamically for that matter,
in the given code. We can get the function app to produce a non-bottom
list value whose dynamic size differs from its size type (and whose
static size is patently not the arithmetic sum of the static sizes of
the arguments).

The solution in this message relies entirely on Haskell type system;
there are no trusted terms. An attempt to write a terminating term
that is to produce a list whose length differs from that stated in the
term's type will be caught by the type checker at compile time.

 {-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}

 module LL where

 data Z; data S a

First we state the Sum constraint:

 class Add n m p | n m - p
 instance Add Z a a
 instance Add n (S m) p = Add (S n) m p

Now we derive a number-parameterized list. We separate the shape
type of the list from the type of the list elements:

 data Nil  len a = Nil deriving Show
 data Cons b len a = Cons a (b a) deriving Show

The constraint `List f' holds iff f is the shape type of a valid list:

 class List ( lst :: * - * )
 instance List (Nil Z)
 instance (Add (S Z) n m, List (tail n)) = List (Cons (tail n) m)

The following `type function' makes sure that its argument is a valid
list. That guarantee is established statically. We should note
that the class List has no members. Therefore, the only terminating term
with the signature `(List f) = f a - f a' is the identity.

 make_sure_it_is_a_list:: (List f) = f a - f a
 make_sure_it_is_a_list = id

 nil:: Nil Z a
 nil = Nil

We let the compiler write out the constraints for us:

 consSig :: a - f l a - Cons (f l) (S l) a
 consSig = undefined
 cons h t | False = consSig h t
 cons h t = make_sure_it_is_a_list$ Cons h t

We can create a few lists:

 testl1 = cons (3::Int) ( cons (2::Int) ( cons (1::Int) nil ) )
 testl2 =   ( cons (2::Int) ( cons (1::Int) nil ) )

The type of testl2 is reasonable:

testl2 :: Cons (Cons (Nil Z) (S Z)) (S (S Z)) Int

If we try to cheat and write
 consSig :: a - f l a - Cons (f l) (S (S l)) a
the typechecker will point out that 'Z' is not equal to 'S Z' when
typechecking testl1 and testl2.

We can now handle Append:

 class Append l1 l2 l3 | l1 l2 - l3 where
 appnd :: l1 a - l2 a - l3 a

 instance Append (Nil Z) l l where
 appnd _ l = l

 instance (Append (t n) l (t' n'), List (t' n'))
 = Append (Cons (t n) (S n)) l (Cons (t' n') (S n')) where
 appnd (Cons h t) l = cons h (appnd t l)
 
We had to be explicit with types in the latter instance. The types
must correspond to the term; the typechecker will tell us if they do
not.

We now attempt to verify the sum of lengths property. We attach the
desired constraints using the partial signature trick. This saves us
trouble enumerating all other constraints.

 constraintAdd:: Add l1 l2 l3 = (f1 l1 a) - (f2 l2 a) - (f3 l3 a)
 constraintAdd = undefined

 vapp l1 l2 | False = constraintAdd l1 l2
 vapp l1 l2 = appnd l1 l2

Perhaps we should move to Cafe?
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Dependent Types in Haskell [was: Eliminating Array Bound Checking through Non-dependent] types

[Martin Sulzmann]

There's a potentially confusing typo.

  append Nil ys = Nil 

should be replaced by

append Nil ys = ys

Thanks to Ketil for pointing this out.

Martin
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Dependent Types in Haskell [was: Eliminating Array Bound Checking through Non-dependent] types

[MR K P SCHUPKE]

Just a couple of quick points...

Why store the length along with the list, the length is stored
using type level naturals (Succ | Zero) but these are identical
to the recursion pattern in a List (Cons | Nil) - therefore it
is no less work than having a length function which converts
from one to the other (Cons x - Succ, Nil - Zero), so
it is really redundant having both.

Second you can express append in a much simpler and readable
way in Haskell using type classes:

-

data Nil deriving Show
data List a = Cons a (List a) deriving Show

class Append l l' l'' | l l' - l'' where
   append :: l - l' - l''
instance List l' = Append Nil l' l' where
   append _ l' = l'
instance Append l l' l'' = Append (Cons a l) l' (Cons a l'') where
   append (Cons a l) l' = Cons a (append l l')

-

Thats the complete definition, no need for extra stuff or
complex exqualities or casts...

Doesn't look too bad to me.

Keean.
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Dependent Types in Haskell [was: Eliminating Array Bound Checking through Non-dependent] types

[MR K P SCHUPKE]

Actually the data statement wasnt quite right:

data Cons a b = Cons a b

Would work, but now there is nothing keeping each
element in the list as the same type,

I guess we could add a class to constrain to a normal list,,,

class List l x
instance List Nil x
instance List l x = List (Cons x l) x

Erm, which is of course what I meant in the first place 

Keean.
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Dependent Types in Haskell [was: Eliminating Array Bound Checking through Non-dependent] types

[Martin Sulzmann]

The append example is meant to make a general point about
the connection between dependent types and Haskell with
extensions. 

I know that the example itself is rather trivial, and
DML/index types, Omega, Haskell+GAD and Chameleon might
seem as too big canons for a rather small target.

  Second you can express append in a much simpler and readable
  way in Haskell using type classes:
  
  -
  
  data Nil deriving Show
  data List a = Cons a (List a) deriving Show
  
  class Append l l' l'' | l l' - l'' where
 append :: l - l' - l''
  instance List l' = Append Nil l' l' where
 append _ l' = l'
  instance Append l l' l'' = Append (Cons a l) l' (Cons a l'') where
 append (Cons a l) l' = Cons a (append l l')
  
  -
  
  Thats the complete definition, no need for extra stuff or
  complex exqualities or casts...
  
  Doesn't look too bad to me.
  

Good, I was waiting for some type class trickery :)
You turn clauses into instance declarations.
This will only work for terminating programs!

Martin
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Re: Dependent Types in Haskell [was: Eliminating Array Bound Checking through Non-dependent] types

[Conor T McBride]

Hi Martin
Martin Sulzmann wrote:
Hi,
Inspired by Conor's and Oleg's discussion let's see which
dependent types properties can be expressed in Haskell (and extensions).
I use a very simple running example.
[..]
We'd like to statically guarantee that the sum of the output list
is the sum of the two input lists.
A lovely old chestnut. I think I wrote that program (in Lego plus
programming gadgets) back in 1998.
[..]
Each list carries now some information about its length.
The type annotation states that the sum of the output list
is the sum of the two input lists.
[Conor: I don't know whether in Epigram you can specify the above property?]
It's basic stuff. Here's the Epigram source, ab initio, which I knocked
up in about 30 seconds (the precise layout is the responsibility of my
suboptimal prettyprinter):
--
  (   n : Nat   !
data (-!  where (! ;  !-!
 ! Nat : * )! zero : Nat )! suc n : Nat )
--
 (   n, m : Nat   !
let  !!
 ! plus n m : Nat )
 plus n m = rec n
 { plus x m = case x
   { plus zero m = m
 plus (suc n) m = suc (plus n m)
   }
 }
--
 ( X : *   !
 ! !
 ! n : Nat !( x : X ;  xs : Vec X n !
data !-!  where (--! ;  !---!
 ! Vec X n !! vnil :   !!vcons x xs :   !
 !  : *)!   Vec X zero )!  Vec X (suc n))
--
 (   xs : Vec X n ;  ys : Vec X m   !
let  !--!
 ! vappend xs ys : Vec X (plus n m) )
 vappend xs ys = rec xs
 { vappend x ys = case x
   { vappend vnil ys = ys
 vappend (vcons x xs) ys = vcons x (vappend xs ys)
   }
 }
--
These programs were developed interactively: I only had to write the
type signatures and the right-hand sides. Under those circumstances,
= rec xs and = case x are rather less effort than typing the
left-hand sides by hand. Moreover they provide guarantees of totality
(structural recursion  exhaustiveness of patterns). I'm sorry I can
only send this program in black-and-white. The editor uses foreground
colour to indicate the status of each identifier and background colour
to indicate the typechecker's opinion of each subexpression.
You'll notice (or perhaps you won't) that there's rather a lot of type
inference going on, both in figuring out indices, and in figuring out
which variables should be implicitly quantified.
You may also notice the number of fingers I need to lift to convince
the machine that the arithmetic condition is satisfied. The definition
of plus is sufficient: the marvellous thing about computation is that
computers do it. You get partial evaluation for free, but if the
constraints require more complex algebra, you have to do the work.
Or teach a computer to do the work, hence the project to implement
a certified Presburger Arithmetic solver in Epigram: that seems a
worthy occupation for the other ten fingers. Or a PhD student.
I like DML/index types but both systems are rather special-purpose. 
There might be other program properties which cannot be captured
by index types.
Not half. See `The view from the left' by myself and James McKinna
for a typechecker (for simply-typed lambda-calculus) whose output is
the result of checking _its input_.
[..]
Tim Sheard argues that no predicates other than equality are
necessary. Here's an adaptation of a Omega example I found 
in one of his recent papers.
This observation dates back to Henry Ford: `you can have any colour
you like as long as it's black'. In a more technical context, it's
certainly a lot older than me. Of course, it's a no-brainer to
turn constraint-by-instantiation into constraint-by-equation if you
have the right notion of equality. You have to deal somehow with
the situation where things of apparently different types must be
equal, but where the types will be identified if prior constraints
are solved. One approach can be found in my thesis.
To me it seems rather tedious to use (plain) Haskell for dependent types
programming.
Absolutely. But the fact that it's to some extent possible suggests
that we could, if we put our minds to it, make it less tedious without
fundamentally messing up anything under the bonnet.
Cheers
Conor
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Dependent Types in Haskell [was: Eliminating Array Bound Checking through Non-dependent] types

[MR K P SCHUPKE]

This will only work for terminating programs!

Interesting point, but thats because all the operations are at
the type level - therefore if a type is unknown at compile time
we cannot produce a program. 

With this type class stuff values can depend on types, but
not the other way around. You can sort of do reification
(types depend on values) for limited finite cases where
it ends up getting implemented as dictionary passing.

an example of reification is:

class (NotNegative m,NotNegative n) = ReifyNotNegative m t i n w where
reifyNotNegative :: Integral i = m - t - i - n - w
instance NotNegative n = ReifyNotNegative Zero t i n w where
reifyNotNegative _ _ _ _ = error Number to be reified exceeds maximum range.
instance (NotNegative n,ReifyNotNegative m t i (Suc n) w,Ctrl.Apply t n w)
= ReifyNotNegative (Suc m) t i n w where
reifyNotNegative (Suc m) t i n
| i0 = reifyNotNegative m t (i-1) (Suc n)
| otherwise = Ctrl.apply t n

(The apply in the above is a 'prolog' like apply, where 't' is a unique
type used to identify the 'function' to apply)



Anyway in this way the whole types depending on values issue is
sidestepped.

Keean.
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Dependent Types in Haskell [was: Eliminating Array Bound Checking through Non-dependent] types

[Martin Sulzmann]

Hi,

Inspired by Conor's and Oleg's discussion let's see which
dependent types properties can be expressed in Haskell (and extensions).
I use a very simple running example.

-- append.hs
-- append in Haskell
data List a = Nil 
| Cons a (List a) 

append ::  List a - List a - List a 
append (Cons x xs) ys = Cons x (append xs ys)
append Nil ys = Nil 

We'd like to statically guarantee that the sum of the output list
is the sum of the two input lists.

In Hongwei Xi's DML or index types a la Christoph Zenger, we can write
the following.

-- append in DML/index types
-- I use a slightly different syntax compared to DML
data List a n = Nil where n=0
  | Cons a (List a m) where n=m+1

append ::  List a l - List a m - List a (l+m)
append (Cons x xs) ys = Cons x (append xs ys)
append Nil ys = Nil 

Each list carries now some information about its length.
The type annotation states that the sum of the output list
is the sum of the two input lists.

[Conor: I don't know whether in Epigram you can specify the above property?]

I like DML/index types but both systems are rather special-purpose. 
There might be other program properties which cannot be captured
by index types.

In the latest Chameleon version, we can encode the above DML/index
types program as follows.

[Side note: I encode dependent types in terms of singleton types]

-- append.ch
-- Chameleon encoding of append in DML/index types

-- encoding of arithmetic
data Zero
data Succ x

-- we introduce a ternary predicate symbol Add l m n
-- which models l+m=n 
-- in my encoding I assume that l and m are given
hconstraint Add
rule Add l m n, Add l m n' == n=n'
rule Add Zero m n == m=n
rule Add (Succ l) m n == Add l m n', n=Succ n'

-- type indexed data type
-- we keep track of the length of the list
data List a n =  (n= Zero) = Nil 
| forall m. Add (Succ Zero) m n = 
Cons a (List a m) 

append ::  Add l m n = 
   List a l - List a m - List a n
append (Cons x xs) ys = Cons x (append xs ys)
append Nil ys = Nil 


Tim Sheard argues that no predicates other than equality are
necessary. Here's an adaptation of a Omega example I found 
in one of his recent papers.

-- append2.ch
-- we introduce terms to represent addition
data Z
data S n

data Sum w x y =
 (w=Z, x=y) = Base
   | forall m n. (w=S m, y=S n) = Step (Sum m x n)

data Seq a n =
 (n=Z) = Nil
   | forall m. (n=S m) = Cons a (Seq a m)

app :: Sum n m p - Seq a n - Seq a m - Seq a p
app Base Nil ys = ys
app (Step p) (Cons x xs) ys = Cons x (app p xs ys)


Well, now that we have compiled away arithmetic, why not get rid
of equality? I rely on encoding trick used by Cheney, Hinze, Weirich,
Xi and most likely many others.


-- append3.hs
-- we introduce terms to represent equality

data E a b = E (a-b,b-a)
-- a silent assumption is that for each monomorphic value E (g,h)
-- functions g and h represent the identity
-- can't be enforced by Haskell, must be guaranteed by the programmer

data Z = Z
data S n = S n


data Sum w x y =
 Base (E w Z) (E x y)
   | forall m n. Step (Sum m x n) (E w (S m)) (E y (S n))

data Seq a n =
 Nil (E n Z)
   | forall m. Cons a (Seq a m) (E n (S m))


app :: Sum n m p - Seq a n - Seq a m - Seq a p
app (Base (E (g1,h1)) (E (g2,h2))) (Nil (E (g3,h3))) ys = 
cast2 (E (g2,h2)) ys
app (Step p' (E (g1,h1)) (E (g2,h2))) (Cons x xs (E (g3,h3))) ys =
   Cons x (app p' (cast2 (E (cast1 (g1.h3),cast1 (g3.h1))) xs) ys) 
   (E (g2,h2))
-- some magic, gs, hs and casts refer to term operations to mimic
-- type-level equality operations. Note that if we erase all Es, gs,
-- hs and casts we obtain append2.ch

cast1 :: (S a-S b)-a-b
cast1 f a = let S b = f (S a)
in b
cast2 :: E m p - Seq a m - Seq a p
cast2 (E (g1,h1)) (Nil (E (g2,h2))) = (Nil (E (g2.h1, g1.h2)))
cast2 (E (g1,h1)) (Cons x xs (E (g2,h2))) = (Cons x xs (E (g2.h1,g1.h2)))


Conclusion:

Note that append3.hs runs under Haskell.
append2.ch runs under Omega, Haskell extension with generalized data
types and Chameleon (note that append2.ch uses Chameleon syntax for
data type definitions!).
append.ch runs under Chameleon. 
To me it seems rather tedious to use (plain) Haskell for dependent types
programming.

Martin
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Eliminating Array Bound Checking through Non-dependent types

[Conor T McBride]

Hello again
Me:
What if I don't trust your kernel?
[..]
What's the downloadable object that can be machine-checked to satisfy
my paranoid insurance company?
Oleg:
I hope that you can forgive me if I reply by
quoting the above two paragraphs back to you, with the substitution 
s/kernel/compiler/.

What if I don't trust your compiler?
I have heard a similar question asked of J. Strother Moore and
J. Harrison. J. Strother Moore said that most of ACL2 is built by
bootstrapping, from lemmas and strategies that ACL2 itself has
proven. However, the core of ACL2 just has to be trusted.
It's not an issue of forgiveness. I actively encourage such questions,
of myself and other people. I'd also recommend this paper by Randy
Pollack:
  `How to believe a machine-checked proof'
  http://www.dcs.ed.ac.uk/home/rap/export/believing.ps.gz
But the one-line summary is `by rechecking it independently'.
Of course, we'll never achieve _certainty_ in any absolute
sense, but we can do a lot better than `I can't show you the
evidence for security reasons, but there's no doubt that...'.
In order to do that, you need more than a machine which
says `yes'. You need a language of evidence which is simple
enough that people can write their own checker in whatever way
they choose. Martin-Loef's type theory provides a source of
good candidates for such a language of evidence. Its core
proof-checking/type-checking algorithm is very small. This is
what comes out the other end of the Epigram elaborator.
[..]
Hongwei Xi's code contains the evidence I'm asking for.
The verification conditions are added by hand in the program as
annotations, just as yours are annotations outside the program.  His
are checked by Presburger arithmetic, just as yours could be.
Actually, as far as the PLDI'98 paper is concerned, they specifically say
they do not use the full Presburger arithmetics. Rather, they solve
the constraints by Fourier variable elimination. Anyway, even if
the various elaboration and decision rules are proven to be sound and
complete, what is the evidence that their implementation in the
extended SML compiler is also sound and complete?
Another very good question. Every time you appeal to a proof-search
oracle or to an axiomatization of a library, or anything which hides
the evidence, the amount of stuff you `just have to trust' gets
bigger, and the harder it is to perform independent rechecking.
But what if some bright spark (volunteers welcome) were to implement
Presburger Arithmetic in one of the following ways...?
  (1) External to the system, but outputting checkable proof terms,
instead of just `yes' or `no'.
  (2) Within the system, with a checkable proof that its yea be
yea and its nay be nay. [Traditional implementation and
correctness proof.]
  (3) Within the system, with a type which actually guarantees
what the algorithm proves in the first place. [The
`two-level' approach.]
The conclusion specifically states that the algorithm is currently
incomplete.
Clearly, soundness is more important. But it is nice to have a good idea
which problems the machine will get and which it won't.
Me:
...this proposition is false. The bounds function returns bounds which
are outside the range of the array when the array is empty.
You'll notice that Hongwei Xi's program correctly handles this case.
Don't get me wrong: I think your branded arrays and indices are a very
good idea. You could clearly fix this problem by Maybe-ing up bbounds
or (better?) by refusing to brand empty arrays in the first place.
Oleg:
I have noticed that the branding trick would work very well with
number-parameterized types. The latter provide missing guarantees, for
example, statically outlaw empty arrays. Hongwei Xi's code has another
neat example: a dot product of two arrays where one array is
statically known to be no longer that the other. Number-Parameterized
types can statically express that inequality constraint too.
Yes, of course. And any dependently typed solution to these problems
would naturally parametrize the data-structures by their size,
represented as ordinary numbers. Statically expressing the constraints
is easy.
The abstract `brand' is just a type-level proxy for the bounding
interval, and the library of operations provides interval-respecting
operations on indices. This is a very neat solution in Haskell, but it
goes round an extra corner which isn't necessary with dependent types,
where you can just talk about the interval directly. The library-writer
would develop and verify the same convenient operations for working
with intervals and indices; the proofs would be independently
recheckable terms in type theory.
The
Number-Parameterized types paper considers a more difficult example --
and indeed the typechecker forced me to give it a term that is
verifiably a proof of the property (inequality on the sizes) stated in
term's inferred type. The typecheker truly demanded a proof; shouting
didn't help

Re: [Haskell] Eliminating Array Bound Checking through Non-dependent types

[oleg]

Hello!

Bjorn Lisper wrote:

 What is the relation to the sized types by Lars Pareto and John Hughes?

It is orthogonal and complementary, as the message in response to
Conor T. McBride indicated.

 What is the relation to classical range analyses for (e.g.) array index
 expressions, which have been known for a long time for imperative languages?

It is just like the classical range analysis, but _reified_ in the
programming language itself. Given a piece of code:

finda x arr = loop lo
where (lo,hi) = bounds arr
  loop i = if i = hi then
  if x == arr ! i then Just i
  else loop (i + 1)
   else Nothing

the analysis sees that 'i' starts at the lower bound of 'arr' and is
incremented afterwards. When the analysis sees the test i = hi it
infers that in the `then' branch of that test `i' does not exceed the
upper bound of the array. Therefore, the indexing operation `arr ! i'
is safe and no range check is needed.

In the `branding' framework, the programmer makes the result of the
test i = hi and the corresponding implication that `i' is in range
known to the type system, by branding the index `i'. To be more
precise, the programmer would replace the first `if' statement with
if_in_range:: (Ix i) = i - BArray s i e - (BIndex s i-r)
  - r -r
if_in_range i arr on_within_range on_outside_rage ...
If `i' turns out to be in range, that fact would be recorded by
passing to the continuation on_within_range a branded index. Thus the
logical implication that was implicit in the range checker is made
explicit to the typechecker here.

 A program analysis like range analysis is not exact, of course: it must make
 safe approximations sometimes and will sometimes say that an array index
 might be out of bounds when it actually won't. In your framework, this seems
 to correspond to the fact that you must verify your propositions about index
 expressions.

True, just as the range analysis must verify the rules of the
analysis. The difference is that the conventional range analyzer is a
part of the _compiler_, typically hidden from view (of a regular
programmer). Here, the analyzer is a part of a _library_.

It is also true that our analysis can't be exact: if the code includes 
let i = very_complex_function j
and we know that j is in range, it may be very difficult to ascertain
that 'i' will always be in range. In that case, we do the following
let j_unbranded = unbrand j
i = very_complex_function j_unbranded
in if_in_range i arr on_within_range on_outside_rage

That is, we intentionally forget the branding information, do a
complex index transformation, followed by a run-time witnessing to
recover the branding. If we somehow know that very_complex_function
keeps its result in range, we can replace `on_outside_rage' with the
function that raises an exception, crashes the computer, etc. If we
are not sure if `i' is in range, then our program 
must do the range check anyway; if `i' turns out of range, the
program should do what the algorithm prescribes in that case. The
upshot is that `if_in_range' makes the programmer explicitly consider the
consequences of the range check. We turn the range check from a
routine safety check into an algorithmically significant decision.

Incidentally, if we can prove that `very_complex_function' leaves the
index in range, then we can make the function return a branded index,
and thus eliminate the if_in_range check above. Because the creation
of a branded index can only be done in a trusted kernel, we must put
such a function into the kernel, after the appropriate rigorous
verification -- perhaps formal verification.
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell