Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.haskell > #476 > unrolled thread

Typing in Haskell

Back to article view | Back to comp.lang.haskell

Contents

  Typing in Haskell ivan.moony@gmail.com - 2018-01-07 01:53 -0800
    Re: Typing in Haskell Paul Rubin <no.email@nospam.invalid> - 2018-01-07 10:33 -0800
      Re: Typing in Haskell ivan.moony@gmail.com - 2018-01-07 12:33 -0800
        Re: Typing in Haskell polymorph self <jackvanc3@gmail.com> - 2018-01-09 14:35 -0800

#476 — Typing in Haskell

Hi all :)

I'm not a regular member of this group and I'm just stopping by to ask some questions, hoping someone would have a patience to answer them.

I don't have a much experience in functional programming, but I have read a certain amount of theory papers and I want to build a new type system anyway. I'm wondering if certain properties I want to achieve already exist in Haskell and company.

I want to mix in Boolean operators and/or/not with type checker. That way, when type-checking each iteration in curried function, I want to check it against a Boolean expression like:

((is of type x) OR (is of type y)) AND NOT (is of type z)

It would be something like set algebra, dealing with unions, intersections and complements, but implemented using basic Boolean operators.

I'm aware of sum and product types, but I still can't wrap my head around above expression without implementing it at low level, directly into type system. Would this kind of Boolean type checking be something new, or it is something that is already achievable in existing functional languages?

Thank you for your time,
Ivan

[toc] | [next] | [standalone]

#478

ivan.moony@gmail.com writes:
> ((is of type x) OR (is of type y)) AND NOT (is of type z)

In Haskell, every term has exactly one (maybe polymorphic or quantified)
type, and that type is known at compile time.  So an expression like the
above makes no sense.  You don't have to test whether thing is of type
x, since you already know.

Maybe you want type classes?  What is an example of something you would
use the feature for?

[toc] | [prev] | [next] | [standalone]

#479

> What is an example of something you would
> use the feature for?

For example, if we introduce imaginary * as and, + as or, - as not, how could we form the semantically same type as:

foo: ((x + y) * -z) -> w

I'm defining x, y, z and w previously, as some existing types. In this example, function foo has a single parameter that accepts an element of the set ((x union y) intersect (not z)).

It seems it is not a new idea. I've got some answers at: https://stackoverflow.com/questions/48139262/boolean-type-checking

these are two relevant papers I got from there:
http://www.cs.cmu.edu/~joshuad/papers/intcomp-jfp/Dunfield14_elaboration.pdf
https://www.irif.fr/~gc/papers/icalp-ppdp05.pdf

[toc] | [prev] | [next] | [standalone]

#481

On Sunday, January 7, 2018 at 3:33:09 PM UTC-5, ivan....@gmail.com wrote:
> > What is an example of something you would
> > use the feature for?
> 
> For example, if we introduce imaginary * as and, + as or, - as not, how could we form the semantically same type as:
> 
> foo: ((x + y) * -z) -> w
> 
> I'm defining x, y, z and w previously, as some existing types. In this example, function foo has a single parameter that accepts an element of the set ((x union y) intersect (not z)).
> 
> It seems it is not a new idea. I've got some answers at: https://stackoverflow.com/questions/48139262/boolean-type-checking
> 
> these are two relevant papers I got from there:
> http://www.cs.cmu.edu/~joshuad/papers/intcomp-jfp/Dunfield14_elaboration.pdf
> https://www.irif.fr/~gc/papers/icalp-ppdp05.pdf

check out learn you a haskell for great good homy!

[toc] | [prev] | [standalone]

Back to top | Article view | comp.lang.haskell

csiph-web