Expected a Numeric type but inferred a Value type

[taguniversalmachine]

Hi,

I keep getting the same error whenever I try to add a type annotation to my code, and if I remove the annotation code further down fails due to insufficient type information so I am stuck.

This is the code:

type Transition = (Integer,Bit)

//decider : Bit -> [Transition] -> [Transition] -> [Transition]
decider bit redperm blueperm = if bit == 1 then redperm else blueperm

// Transitions, the index of the tuple within the list
// indicates the state number, with the first tuple at index 0 being the Decider
// and state 8 being the output and not needing a memory location
// For the transition function in the second part of the tuple, we use
// 0 for no change (+) and 1 for invert (-)
red = [(1,0),(4,0),(3,0),(6,1),(7,1),(2,1),(8,1),(5,0)]
blue  = [(1,0),(3,1),(5,1),(4,0),(6,0),(8,0),(7,0),(2,1)]

message = [1,0,1,0,0,1,1,1]

// Populate the memory locations with initial values

redMem  = [-1, -1, -1, -1, -1, -1, -1, -1]      // Initial value for red permutation memory
blueMem = [-2, -2, -2, -2, -2, -2, -2, -2]      // Initial value for blue permutation memory

//type Permuter = [(Integer, Integer, Integer)]
//red_permuter : Permuter
red_permuter = [ (transition, invert,  mem_cell) | (transition, invert) <- red|  mem_cell <- redMem]
// [(1, 0, -1), (4, 0, -1), (3, 0, -1), (6, 1, -1), (7, 1, -1),
//  (2, 1, -1), (8, 1, -1), (5, 0, -1)]

blue_permuter = [ (transition, invert,  mem_cell) | (transition, invert) <- blue | mem_cell <- blueMem]
// [(1, 0, -2), (3, 1, -2), (5, 1, -2), (4, 0, -2), (6, 0, -2),
//  (8, 0, -2), (7, 0, -2), (2, 1, -2)]

// Push function to move bits through a permuter and obey the transition function (+/-)
// the function will return the bit in the last state and then shift the bits in the memory locations
// along in the order the transitions are defined

//last_bit : [(Integer, Integer, Integer)] -> Integer
last_bit permuter  = (permuter ! 0).2

The part that fails is the type declaration for Permuter, it is just a list of 3-tuples. The last line is where I am stuck, I am trying to access the last element of the list and then retrieve the third element of the tuple.

Even just the type definition in the interactive terminal fails:

Cryptol> type Permuter = [(Integer, Integer, Integer)]

[error] at <interactive>:11:18--11:45:
  Incorrect type form.
    Expected: a numeric type
    Inferred: a value type

This is how Cryptol is inferring it:

red_permuter :
  {a, b, c} (Ring b, Literal 1 c, Literal 1 b, Literal 8 a) => [8](a, c, b)

which just seems odd to me, it's technically correct but why is it literally encoding '8' into the type just because it sees an 8 in there, whereas I am providing it with a correct and more general type definition but it rejects it.

Any pointers as to what I am doing wrong?

[RyanGlScott]

Hi @taguniversalmachine! This appears to be an issue with Cryptol moreso than with SAW, so I've transferred this issue to the Cryptol repo for increased visibility.

[RyanGlScott]

The issue with your code is that you are trying to define sequences like [Transition] and [(Integer, Integer, Integer)]. This doesn't make sense in Cryptol's type system, as Cryptol sequence types are indexed by the length of the sequence. For example, your type signature for red_permuter would work if you wrote:

type Permuter = [8](Integer, Integer, Integer)

This says that Permuter expects sequences with eight elements. (You also observed a more general type that Cryptol inferred for red_permuter, which is slightly more polymorphic over the integer types involved. But more importantly, it still requires the [8] part.)

I think you might be used to list types in other functional languages like Haskell, which let you write list types of unspecified lengths. Cryptol does not support this, however. All sequences must be indexed by their length. This is a pretty fundamental part of Cryptol's type system, and one that does take some getting used to.

[taguniversalmachine]

Ah ok yeah that makes sense, it works now, and yes I was getting that from Haskell, but it makes sense that Cryptol would need data structures that directly map to hardware, more like Ada. Thanks very much for the help, that was driving me crazy.