#type (:&) Source

Operator alias for Network.Ethereum.Web3.Solidity.Size.DCons (right-associative / precedence 6)

#type (:%) Source

Operator alias for Network.Ethereum.Web3.Solidity.Size.DTwo (right-associative / precedence 6)

#DOne Source

data DOne :: Digit -> DigitList


#DCons Source

data DCons :: Digit -> DigitList -> DigitList


#KnownSize Source

class KnownSize (d :: DigitList)  where


  • sizeVal :: DLProxy d -> Int

    Given proxy of a Digit returns a number it represents

    1995 == sizeVal (DLProxy :: DLProxy (D1 :& D9 :& D9 :% D5))


#DLProxy Source

data DLProxy (d :: DigitList)

For types of kind Type there is already Type.Proxy. this is basicity the same thing but for types of kind DigitList. Documentation of Type.Proxy module has motivation for why would one need a Proxy for some type which we will not cover here.


#IntSize Source

class (KnownSize n) <= IntSize n 

IntSize is empty class, if there is instance of IntSize for some number it means there is solidity type int of that size specific number in like int16, int24 ... int256


#ByteSize Source

class (KnownSize n) <= ByteSize n 

ByteSize is empty class, if there is instance of ByteSize for some number it means there is solidity type bytes of that size specific number in like bytes1, bytes2 ... bytes32


#Inc Source

class Inc (input :: DigitList) (output :: DigitList) | input -> output

This is like inc but in type-level for DigitList, it computes increment of it's input. It could be used like this for example:

cons :: forall a n nInc. Inc n nInc => a -> Vector n a -> Vector nInc a
uncons :: forall a n nDec. Inc nDec n => Vector n a -> { head :: a, tail :: Vector nDec a }

see Network.Ethereum.Web3.Solidity.Vector


#Digit Source

data Digit :: Type

Digit is a new Kind used to represent digits in base 10 counting system. Alongside this kind we have types D0, D1 ... D9, which have kind Digit. This two parts conceptually translate to this sum type: We could represent all digits used in base 10 counting counting system like this:

data Digit = D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9

here Digit has kind Type and D0, D1 ... are values of type Digit, to be able to represent this digits in type-level we need to have distinct types for each such value when we just have one Digit for all of them. We could create empty types for each digit like data Void. But they will have kind Type and it's not good as one could use them incorrectly. for example this will compile:

data D1
data D2
data D9

x :: Array D1
x = []

It compiles as Array kas kind Type -> Type, i.e. it's type constructor, it takes a Type and returns Type. We want such program to be rejected by compiler, so to be more type-safe, we create new kind Digit, and our types representing digits, will be of this kind instead of "default" kind Type.

foreign import kind Digit
foreign import data D0 :: Digit
foreign import data D2 :: Digit
foreign import data D3 :: Digit

now you can't have x :: Array D3 will not compile at all.

#DProxy Source

data DProxy (d :: Digit)

Same as DLProxy but for types of kind Digit


#DigitList Source

data DigitList :: Type

As we have kind Digit we introduce kind DigitList for list of digits. in value level this could be represented as:

data DigitList = DCons Digit DigitList | DOne Digit

Note: you can't have empty list here as terminal node takes a Digit. the builtin Array in purescript could be defined like this

foreign import data Array ∷ Type -> Type

Similarly we are defining DCons and DOne, but with kinds we have defined already:

foreign import data DCons ∷ Digit -> DigitList -> DigitList
foreign import data DOne ∷ Digit -> DigitList

Now we can represent number 1995 in type-level like this:

type MyNum = DCons D1 (DCons D9 (DCons D9 (DOne D5)))

Yes it's too verbose, that's why we have type-level operator :& for DCons like : for Cons of List.

infixr 6 type DCons as :&

type MyNum = D1 :& D9 :& D9 :& DOne D5

the _ :& DOne _ part is a bit annoying, so we fix it with a new type alisa for such types and an operator for it :%:

type DTwo d1 d2 = d1 :& DOne d2
infixr 6 type DTwo as :%

type MyNum = D1 :& D9 :& D9 :% D5

Nice and sweet. Note in typeclass instances type aliases can't be used, which DTwo and :% are. so this will not compile instance myInstance :: SomeCls (D1 :% D0) instead it should be written as instance myInstance :: SomeCls (D1 :& DOne D0)

#DTwo Source

type DTwo d1 d2 = d1 :& (DOne d2)

#IncP Source

class IncP (input :: DigitList) (output :: DigitList) (carry :: Boolean) | input -> output carry


#IncD Source

class IncD (input :: Digit) (output :: Digit) (carry :: Boolean) | input -> output carry


#KnownDigit Source

class KnownDigit (d :: Digit)  where



#DigitCount Source

class DigitCount (d :: DigitList)  where