1. Forum
  2. Usenet
  3. COMP.LANG.HASKELL

  • Typing in Haskell

    From ivan.moony@gmail.com@21:1/5 to All on Sun Jan 7 01:53:21 2018
    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

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Paul Rubin@21:1/5 to ivan.moony@gmail.com on Sun Jan 7 10:33:56 2018
    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?

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From ivan.moony@gmail.com@21:1/5 to All on Sun Jan 7 12:33:08 2018
    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

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From polymorph self@21:1/5 to ivan....@gmail.com on Tue Jan 9 14:35:31 2018
    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!

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)