mlabs-haskell / lambda-buffers

LambdaBuffers toolkit for sharing types and their semantics between different languages
https://mlabs-haskell.github.io/lambda-buffers/
Apache License 2.0
29 stars 0 forks source link

Sum and Product type expressions #51

Closed bladyjoker closed 1 year ago

bladyjoker commented 1 year ago

Hey, we need to establish what type bodies we support and in which context.

Currently, we only support Sum of Tuples.

sum Foo a = MkFoo Int a | MkBar (Maybe a) String

However, the following questions arise:

  1. Do we enable Record expressions in Sum context?
    sum Foo a = MkFoo {foo :: Int, fooz :: a} | MkBar { bar:: Maybe a, baz :: String}
  2. Do we enable first class Tuples in TyDef context?
    prod Foo a = a Int (Maybe a)

    For example, Haskell tydef codegen for this would be:

data Foo a = MkFoo a Int (Maybe a)
  1. Do we enable first class Records in TyDef context?
rec Foo a = { foo: a , bar:: Int, baz:: (Maybe a)}

For example, Haskell tydef codegen for this would be:

data Foo a = MkFoo { foo: a , bar:: Int, baz:: (Maybe a)}

Please share your thoughts about how that would codegen in different languages:

  1. Haskell
  2. Plutarch
  3. Purescript
bladyjoker commented 1 year ago

Newtypes

For product types, like prod and rec, I'd establish a rule that it goes into a newtype when possible:

prod MyInt = Int
rec MyIntR = { f :: Int }
cstml commented 1 year ago
1. Do we enable `Record` expressions in `Sum` context? 
sum Foo a = MkFoo {foo :: Int, fooz :: a} | MkBar { bar:: Maybe a, baz :: String}

From a KC pov I see no issue. Is there an issue with the CodeGen? You can do this in Rust (example), in Haskell (example), is this doable in something like P'Arch?

2. Do we enable first class Tuples in `TyDef` context?
prod Foo a = a Int (Maybe a)

For example, Haskell tydef codegen for this would be:

data Foo a = MkFoo a Int (Maybe a)

I read this in a few ways:

-- prod Foo a = a Int (Maybe a) 
type Foo a = (a, Int, (Maybe a))
newtype Foo a = Foo (a, Int, (Maybe a))
data Foo a = Foo  a  Int  (Maybe a) 

Unsure which one models what you want the most - is the last one specifically what you want it to be?

3. Do we enable first class Records in `TyDef` context?
rec Foo a = { foo: a , bar:: Int, baz:: (Maybe a)}

For example, Haskell tydef codegen for this would be:

data Foo a = MkFoo { foo: a , bar:: Int, baz:: (Maybe a)}

I don't like the magic of getting a default constructor for it. I'd argue it is confusing for a user and inconsistent with the end result. I think we always have a constructor to avoid confusion.

bladyjoker commented 1 year ago

This is settled.