GaloisInc / ivory

The Ivory EDSL
http://ivorylang.org
BSD 3-Clause "New" or "Revised" License
393 stars 28 forks source link

Question: Using "Simple" Sum Types in Ivory #107

Closed pjones closed 7 years ago

pjones commented 7 years ago

I'm experimenting with Ivory and would like a bit more compile-time safety for some of my types. In Haskell I would normally use a sum type to represent options or states. I know Ivory doesn't directly support enums or sum types but it seems like it should be able to support a type that has an Enum instance by converting it into a numeric type.

For example, consider this type:

data PinMode = Input | Output

And a proc:

pinMode :: Def ('[Uint8, PinMode] ':-> ())
pinMode = undefined

I would like to pass a PinMode value to the pinMode proc and have it converted to a Uint8 (that would then be passed through to some existing C function). As I mentioned above, this could be done using an Enum instance.

For more complicated usages I would love to be able to write Ivory conditionals that emulate a case expression that tests a Uint8 against various data constructors.

So far I've gone down the path of defining instances of IvoryType, IvoryVar, and IvoryExpr. This is where I've gotten stuck though. I'm not really sure at which stage I need to convert my type into a Uint8. I'm assuming that it makes the most sense to create a Uint8 as a literal expression, but I'm not exactly sure how or when I would do that.

Any help would be appreciated. Thanks!

leepike commented 7 years ago

Perhaps try something like this. Assuming you have

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

define

newtype PinMode = PinMode Uint8
  deriving (IvoryType, IvoryVar, IvoryExpr, IvoryEq, IvoryStore, IvoryInit, IvoryZeroVal)

and then

input, output :: PinMode
input  = 0
output = 1

Then unless someone constructs new PinMode constants, the values are constrained.

pjones commented 7 years ago

That's certainly a workable solution. Thank you.