newtype

Stream: lean4

[Pi Lanningham]

Is there a notion of newtype in lean? or should I just use a structure with one field?

[Henrik Böving]

Either that or a def, e.g. ReaderT is defined with a def

[Arthur Paulino]

Do you mean creating your own type? Maybe constant MyType : Type?

[Henrik Böving]

No he means the newtype concept from haskell which is done in lean using a def or a one element structure

[Henrik Böving]

As an example, this is how ReaderT is defined in Lean:

def ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
  ρ → m α

@[inline] def ReaderT.run {ρ : Type u} {m : Type u → Type v} {α : Type u} (x : ReaderT ρ m α) (r : ρ) : m α :=
  x r

Vs haskell:

newtype ReaderT r m a = ReaderT { runReaderT :: r -> m a }

[Pi Lanningham]

So, thinking out loud here, if I wanted to define a type Hash as an alias for ByteArray, I could do

def Hash := ByteArray
structure Message where
  hash : Hash

Is there a Lean-idiomatic way to attach a proof to that? i.e. a hash is any byte array, so long as the size is 32 bytes or something along those lines?

[Arthur Paulino]

Then structure comes in handy:

structure Hash where
  data : ByteArray
  properLength : data.size = 32 := by simp

[Henrik Böving]

Okay multiple things:
First, there is a difference between an alias which would be an abbrev and a def, if you define a type using def it will not inherit the type class instances the type on the right hand side has automatically, if you define it with an abbrev it will.

now is there a Lean idiomatic way to attach a proof to that, yes there are actually multiple, first way would be to just have it as a structure field:

structure LenVec (α : Type u) (n : Nat) where
  list : List α
  len : list.length = n

second way would be using a subtype, example:

-- The rhs of this
def SortedBTree (α : Type u) (β : Type v) [LinearOrder α] : Type (max u v) := {t : BTree α β // Sorted t}

which of these two you pick in which situation I am actually not 100% sure about yet, especially since subtype is just:

structure Subtype {α : Sort u} (p : α → Prop) where
  val : α
  property : p val

I think if you just have value + property use a subtype, if you have more than one value or more than one property a structure with proofs might be better.

[Pi Lanningham]

Ooo, thank you! <3 That's super helpful, both of you

[Arthur Paulino]

The := by simp part of my example is serving as a default proof, if the user doesn't provide one when instantiating the structure

structure Hash where
  data : ByteArray
  properLength : data.size = 2 := by simp

def byteArray2 : ByteArray := ⟨#[3, 4]⟩
def byteArray3 : ByteArray := ⟨#[3, 4, 5]⟩

def h : Hash := Hash.mk byteArray2 -- works

def h' : Hash := Hash.mk byteArray3 -- breaks
-- unsolved goals
-- ⊢ False