ChildsplayOSU / bogl

Haskell implementation of the BoGL language
https://bogl.engr.oregonstate.edu
BSD 3-Clause "New" or "Revised" License
7 stars 1 forks source link

Determine whether we allow comparison between symbols and other btypes #134

Closed alexgrejuc closed 3 years ago

alexgrejuc commented 4 years ago

Previously this was allowed. I heard from @montymxb that this was discussed and changed at some point this summer. Right now, the type system still allows it, but it results in a runtime error. I think we should remove the runtime error and allow it.

I see two options for doing so:

  1. only allow if there exists a type that contains the symbol and the other btype (e.g. Int & {A} allows A == 1 but not B == 1)
  2. always allow it

The example below illustrates why I think it should be allowed in some form:

game G

type Position = (Int, Int)
type Board = Array (3,3) of Int & {X}

b : Board
b!(x,y) = 1
b!(1,1) = X

b ! (1,1) == X results in True and every other position results in a runtime error.

Another common scenario is comparison with Empty.

montymxb commented 4 years ago

Ahhh, didn't think of that, good catch. I'm a fan of the first option, but that means we will have to make a change to the typechecker to recognize explicitly defined values for a type syn, but this comparable to just defining new types, instead of using a synonym (like mentioned in #115). The approach we take will probably be with regard to how we handle that. This might be a good one to discuss in a meeting.

MartinErwig commented 4 years ago

I think this should be allowed. I don't recall why it was cast as illegal.

-- Martin

On Aug 17, 2020, at 12:00 PM, Alex Grejuc notifications@github.com wrote:

Previously this was allowed. I heard from @montymxb that this was discussed and changed at some point this summer. Right now, the type system still allows it, but it results in a runtime error. I think we should remove the runtime error and allow it.

I see two options for doing so:

• only allow if there exists a type that contains the symbol and the other btype (e.g. Int & {A} allows A == 1 but not B == 1) • always allow it The example below illustrates why I think it should be allowed in some form:

game G

type Position = (Int, Int) type Board = Array (3,3) of Int & {X}

b : Board b!(x,y) = X

isX : (Board, Position) -> Bool isX(b, p) = b ! p == X

Another common scenario is comparison with Empty.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe.

alexgrejuc commented 3 years ago

Closed because symbolic values can be compared to other values provided there is a type that contains them both.